safety vs invariant

Stream: Veil

[Mark R. Tuttle]

Could you add a comment in the Property section of the documentation to explain the difference between safety and invariant? I think the answer is "An invariant property must be inductive but a safety property must be merely true in all reachable states and must follow from the invariants."

[George Pîrlea]

They actually mean the same thing. From our CAV paper:
image.png

I'll make it clear in the documentation. Thank you!

[George Pîrlea]

Basically, the meaning of both is invariant, i.e. property that holds in all reachable states.

When you do #model_check, that gets checked explicitly.

When you do #check_invariants, the conjunction of all invariant and safety clauses is taken to be the inductive invariant.