What TLA+ can and can't check

adamddev1

Great write-up. People keep saying "we can just write tests" or more recently "we can use formal verification," thinking these are sufficient safeguards we can use and then relegate all the implementation to LLMs. But the fact is that probabilistic guessing machines can't save them. People can't escape the need to actually understand the things they are building.

rrook

i think part of this is a shortcoming of our programming languages. generally, languages allow for the expression of partial graphs, which makes the verification problem technically challenging. my take is that a language that only exposes closed-graph semantics could help bridge the gap between the model and the implementation, even if not absolute.

sourdecor

I discovered Quint[0] due to this comment[1] on HN. Quint is "an executable specification language [which works in JavaScript] with delightful tooling based on the temporal logic of actions (TLA)". I think it is awesome and anybody interested in TLA+ should check it out. [0]: https://github.com/quint-co/quint [1]: https://news.ycombinator.com/item?id=49865720

ChrisArchitect

Related: The internet discovers TLA+. Now what? https://news.ycombinator.com/item?id=49863600

westurner

From "How did software get so reliable without proof? (1996) [pdf]" (2024) https://news.ycombinator.com/item?id=42425617 : > From "The Future of TLA+ [pdf]" (2024) https://news.ycombinator.com/item?id=41385141 : >> Formal methods including TLA+ also can't/don't prevent or can only workaround side channels in hardware and firmware that is not verified. But that's a different layer. >> Things formal methods shouldn't be expected to find: Floating point arithmetic non-associativity, side-channels

singron

I love this. This is great to read if you are trying to use TLA+ for something. In a different vein, another thing TLA+ isn't great at is modeling atomics and in particular weak-memory semantics or anything that's not sequentially consistent. If you translate your algorithm to pcal, it will run as if it was sequentially consistent. If you need to model non-sequential-consistency, then that needs to be spelled out with explicit logic to TLA+, which is probably too complicated and error-prone to do by hand. The C/C++/Rust memory models permit a lot of wacky stuff. I imagine you need to add read caches and writeback buffers for each variable with cache-flushing instructions at appropriate points, but maybe there is a more elegant way to do it. If you use rust, miri and loom both have analyzers that can check some non-sequentially-consistent behavior (and loom doesn't actually implement sequential-consistency at all).

lou1306

Uhm, I can see the desire to simplify, but the passage about "reachability" sounds odd. Sure, TLA+ lets you verify whether P is true in every state of every behavior by checking []P. But a _counterexample_ to that property, if it exist, is _some_ state in _some_ behaviour where P is false. Thus, if your model checker proves []P false, you have indirectly proven E<>!P (where the initial E means exactly "for some behaviour"). Going back to the example, "proving that a game is winnable" should be achievable by model checking the invariant "the game is never winnable" and failing. Or am I missing something here?

IshKebab

IMO TLA+ is not very good. It has super weird syntax, and a whole separate DSL (PlusCal) to give it workable syntax for programs. You can really tell it was created by the same mind as LaTeX. What is the Typst of formal modeling? Another issue is that you end up with a formal model that passes, but then you have still have to convert that to a real language by hand and not make any mistakes.

metabagel

Love the inline footnotes!

maxgashkov

Do we need... TLA++?

spaintech

While both TLA+ and ADA/Spark might be necessary, I haven’t noticed much mention of ADA/SPARK here, which kind of surprised me that they are not used in conjunction as frequent as I might have thought. For some critical software we developed, we used TLA+ for high-level formal specification. As mentioned earlier, transitioning the actual implementation to another language can be challenging, especially if partial hardware bootstrapping is required. We ended up implementing the high-level specification created in TLA+ using ADA/Spark, which minimized our exposure to buffer and assertion failures. However, optimizing the code to meet performance thresholds was at times frustrating and time-consuming, like any low-level implementation with a new tool/language for us. I’m curious about any new tools or workflows for leveraging TLA+ high-level specification implementation into other languages like C and Rust. What approaches are people taking once the formalized specification is verified in TLA+ to complete the implementation? I might be out of the loop, but using TLA+ spec and translate then to other languages hasn’t been a successful use case for LLMs. While they can be helpful, a significant effort is still required to ensure that implementations accurately adhere to the specifications.