Writing correct lock-free and distributed stateful systems in Rust, with TLA+(https://github.com/spacejam/tla-rust)374 points|gfortaine|8 years ago|94 comments
Leslie Lamport: Video course on TLA+(http://lamport.azurewebsites.net/video/intro.html)328 points|kelvich|8 years ago|74 comments
The TLA+ Video Course by Leslie Lamport(https://lamport.azurewebsites.net/video/videos.html)219 points|blopeur|7 years ago|17 comments
A walkthrough tutorial of TLA+ and its tools: analyzing a blocking queue(https://github.com/lemmy/BlockingQueue)213 points|pron|5 years ago|6 comments
TLA+ model checking made symbolic(https://blog.acolyer.org/2019/11/29/tla-model-checking-made-symbolic/)197 points|feross|5 years ago|51 comments
The Future of TLA+ [pdf](https://lamport.azurewebsites.net/tla/future.pdf)195 points|tkhattra|7 months ago|105 comments
Modeling Message Queues in TLA+(https://www.hillelwayne.com/post/tla-messages/)195 points|panic|6 years ago|46 comments
Introduction to TLA+ Model Checking in the Command Line(https://medium.com/@bellmar/introduction-to-tla-model-checking-in-the-command-line-c6871700a6a2)176 points|mbellotti|6 years ago|44 comments
Using TLA+ in the Real World to Understand a Glibc Bug(https://probablydance.com/2020/10/31/using-tla-in-the-real-world-to-understand-a-glibc-bug/)166 points|ingve|4 years ago|76 comments
Formal Methods in Practice: Using TLA+ at ESpark(https://medium.com/espark-engineering-blog/formal-methods-in-practice-8f20d72bce4f)152 points|luu|8 years ago|19 comments
TLA+: design, model, document, and verify concurrent systems(https://lamport.azurewebsites.net/tla/tla.html)148 points|lolptdr|6 years ago|32 comments
Using TLA+ to Understand Xen Vchan(http://roscidus.com/blog/blog/2019/01/01/using-tla-plus-to-understand-xen-vchan/)148 points|technion|6 years ago|12 comments
TLA+ in Practice and Theory, Part 4: Order in TLA+(https://pron.github.io/posts/tlaplus_part4)143 points|hiq|8 years ago|11 comments
Using TLA+ for fun and profit in the development of ElasticSearch [video](https://www.youtube.com/watch?v=qYDcbcOVurc)135 points|ngaut|6 years ago|15 comments
Modeling Redux with TLA+(https://www.hillelwayne.com/post/tla-redux/)132 points|hellerve|7 years ago|33 comments
TLA+ in Practice and Theory, Part 3: The Temporal Logic of Actions(https://pron.github.io/posts/tlaplus_part3)130 points|pron|8 years ago|7 comments
Modeling Adversaries with TLA+(https://www.hillelwayne.com/post/adversaries/)126 points|Supermighty|6 years ago|13 comments
Finding Goroutine Bugs with TLA+(https://www.hillelwayne.com/post/tla-golang/)125 points|headalgorithm|5 years ago|40 comments
Breaking the limits of TLA+ model checking(https://www.hillelwayne.com/post/graphing-tla/)122 points|todsacerdoti|2 years ago|4 comments
Principles of TLA+(https://pron.github.io/posts/tlaplus_part1)121 points|pramodbiligiri|8 years ago|23 comments
TLA+ Action Properties(https://www.hillelwayne.com/post/action-properties/)109 points|ingve|4 years ago|36 comments
Creatively Misusing TLA+(https://buttondown.email/hillelwayne/archive/creatively-misusing-tla/)104 points|iforgetlogins01|2 years ago|7 comments
TLA+ Graph Explorer(https://github.com/afonsonf/tlaplus-graph-explorer)103 points|hwayne|4 years ago|6 comments
Using TLA+ to Model Cascading Failures(https://medium.com/@bellmar/using-tla-to-model-cascading-failures-5d1ebc5e4c4f)98 points|mbellotti|6 years ago|24 comments
