Proofs
- Polychrony - Sigali
- System for verification of reactive systems and discrete controller synthesis
- Timbuk
- Timbuk is a collection of tools for achieving proofs of reachability over Term Rewriting Systems and for manipulating Tree Automata (bottom-up non-deterministic finite tree automata)