4 ms·
The TLA+ tools can do exhaustive model checking, as well as mechanically checked proofs. The proofs typically use an SMT solver to verify them. Of the two I've
by grogers 12y ago
The TLA+ tools can do exhaustive model checking, as well as mechanically checked proofs. The proofs typically use an SMT solver to verify them. Of the two I've only used model checking in a serious way, but you can find Lamport's proofs of things like paxos and have it turn all the theorems green.
- tel 12y agoSMT is still a pretty far cry from type theoretic proof. At the end of the day it's just another kind of exhaustiveness checker.