anvil-verifier/anvil

Implement temporal logic operators in Verus

marshtompsxd opened this issue · 1 comments

marshtompsxd commented

To be able to express and prove liveness properties (#3 ), we need to implement temporal logic operators in Verus. The current implementation is in https://github.com/vmware-research/verifiable-controllers/blob/write_liveness_property/src/spec/liveness_property.rs.

We will evaluate whether it can work as expected by trying to prove the liveness property of the ABC example (#8 ) with the operators.