In short: Spin and TLA+ are "push-button" mechanisms where computer are trying every possible trace of your system to check system state against supplied invari

In short: Spin and TLA+ are "push-button" mechanisms where computer are trying every possible trace of your system to check system state against supplied invariant. Pros: You don't have to think much about your systems thin properties before verifying. Cons: State space explosion so not every real system is a subject to such verification. Coq,Agda: Manual/Semi-manual correctness proof of your system. You can reason about even "infinite" systems with this approach using relatively little computation resources. But to do so you have to gain a _deep_ insight about your system behaviour, computation semantics, network semantics (if distributed system is checked) and other properties. If you are lucky you can proof property under question, even it assumes very large moving parts. If not then you cant tell that this property can be proved at all. So these are more like platforms for quasi-manual deduction. F* is trying to take up a niche between manual proof and quasi-automatic proof using SMT solver for those of theorems which can be proved this way. The problem is that SMT solvers are generally suck, there is no sound theory behind it, so it is more like guessing in my opinion.