&gt; There&#x27;s no easy route for it for beginners<p>And if this post had appeared on a Coq forum, a verification forum or even LtU, I would have said nothing. However, as this is HN, and there are probably many beginners reading this, I thought it very relevant to point out a more beginner-friendly tool as a foray into this interesting subject.<p>&gt; what uses it&#x27;s had in sequential, low-level algorithms<p>This is a fairly recent paper that describes a tool that translates C to TLA+ for verification: <a href="http:&#x2F;&#x2F;www.lsv.ens-cachan.fr&#x2F;Publis&#x2F;PAPERS&#x2F;PDF&#x2F;MLBHB-ftscs15.pdf" rel="nofollow">http:&#x2F;&#x2F;www.lsv.ens-cachan.fr&#x2F;Publis&#x2F;PAPERS&#x2F;PDF&#x2F;MLBHB-ftscs15...</a> It works for concurrent C programs as well as sequential ones.<p>This is an old (old) spec by Lamport of the Win32 Threads API: <a href="http:&#x2F;&#x2F;research.microsoft.com&#x2F;en-us&#x2F;um&#x2F;people&#x2F;lamport&#x2F;tla&#x2F;threads&#x2F;threads.html" rel="nofollow">http:&#x2F;&#x2F;research.microsoft.com&#x2F;en-us&#x2F;um&#x2F;people&#x2F;lamport&#x2F;tla&#x2F;th...</a><p>And again, the choice of TLA+&#x2F;Coq often has much more to do with the community the author belongs to (PL&#x2F;conc-dist algorithms) rather than some specific strengths of the tool.