Sadly I don't think it's possible to represent an infinite trace as a SAT problem, so you can't check any liveness properties (will a good thing eventually happ

Sadly I don't think it's possible to represent an infinite trace as a SAT problem, so you can't check any liveness properties (will a good thing eventually happen) unless you use something more powerful. Promela/Spin and TLA+/TLC use model checkers, TLA+/TLAPS and B/Rodin use theorem provers, Electrum uses an SMT solver.