What TLA+ can and can't check(buttondown.com)
223 points by b-man | 47 comments
Hillel Wayne's Computer Things newsletter post on the limits of what TLA+ can verify, pushing back on claims that TLA+ with AI models will make AI-written code reliable.
#tla-plus on Hacker News
5 stories tagged tla-plus, newest first.
The internet discovers TLA+. Now what?(reasonable.io)
97 points by matt_d | 48 comments
A Reasonable blog post introducing TLA+ and discussing how temporal specifications, proof systems, and AI agents can combine to produce specified, verified software.
In Search of a Compositional Theory of Self-Stabilization(muratbuffalo.blogspot.com)
44 points by matt_d | 3 comments
Blog post on the Metadata blog exploring compositional theories of self-stabilization, using a rely-guarantee TLA+ model of a retry storm and metastable failure.
Systems Correctness Practices at Amazon Web Services(cacm.acm.org)
345 points by tanelpoder | 127 comments
Communications of the ACM practice article by Marc Brooker and Ankush Desai on how AWS uses formal and semi-formal methods to ensure systems correctness.
Raku: A language for gremlins(buttondown.email)
355 points by azhenley | 180 comments
Hillel Wayne's Computer Things newsletter post describing the Raku programming language as a quirky language 'by gremlins, for gremlins'.