Discover and read the best of Twitter Threads about #tlaplus
Most recents (2)
1/ Apalache is Informal’s symbolic checker for #tlaplus that checks your specifications by solving constraints instead of enumerating states. informal.systems/2021/03/08/apa…
2/ How does it work? Apalache translates TLA+ specs using SMT solvers to reason about states & transitions in terms of logic, rather than in terms of individual states & transitions. apalache.informal.systems
3/ Our main goal has been to improve the usability of the model checker by testing the tool with internal customers, which saw 3 issues come up consistently:
- How do I write TLA+?
- Why is Apalache complaining about types?
- Why is Apalache complaining about assignments?
- How do I write TLA+?
- Why is Apalache complaining about types?
- Why is Apalache complaining about assignments?
I have to thank @Hillelogram here for introducing his Twitter following to TLA+. The whole concept doesn't look that wild, but even just a superficial knowledge of it just helped me out by a surprising amount
Started playing around with TLA+ a few days ago, wrote a 70 line spec today (this would probably be a lot shorter if I actually knew what I was doing), and while it didn't show me a fundamental flaw in my system, it helped me realize and check that some mutexes were redundant.
The point is not that I couldn't have convinced myself of the correctness without TLA+, it's rather that I probably would have been too lazy, but with the spec already written, I could just change a few things, rerun the model checker, and gain confidence that this works
