Keywords: temporal, globally, eventually

Ivy has some support for properties in temporal logic. In this logic, the normal expression grammar is augmented with globally <expr> and eventually <expr>.

Temporal properties can be proven with the tactic l2s and tactic invariance tactics.