As I said in another comment, stories like this make people interested in formal methods, and Coq, IMO, would be daunting for most beginners. TLA+ is a good, beginner-friendly entry point to formal methods (and you can slowly progress from specification to model-checking and only then proofs), even if you later choose to move to dependent-type approaches and tools like Coq or F*.<p>&gt; TLA+ is for totally different jobs. Not relevant here.<p>I beg to differ. TLA+ is commonly (as far as the word &quot;commonly&quot; can be used when formal methods are discussed) used to specify and verify programs in C or any other language.<p>It is true that Coq has been used to verify compilers more than TLA+, while TLA+ has been used to verify algorithms (esp. concurrent&#x2F;distributed) more than Coq, but the reason is not because neither could do the other&#x27;s job, but because of their respective progeny. Coq (as all type-theory tools) is closely associated with PL-theory people, who tend to be more attracted to compilers, while TLA+ originated from the software-verification world (mostly Pnueli&#x27;s temporal logic), and created and promoted by Leslie Lamport, most certainly an &quot;algorithms&quot; (specifically distributed&#x2F;concurrent) guy rather than a &quot;PL&quot; guy.<p>BTW, Isabelle is one of the proof engines used by the TLA+ proof system.