What TLA+ can and can't check
buttondown.com
buttondown.com
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.
You have to go into high integrity computing industry and related conferences to see it being used.
It doesn’t fully close the specification gap but if it could be made robust it might be a good tool.
Generating code directly from the high level specification is called, synthesis, and is still in research mode.
Projects like Synquid[0] have come a ways but are still far from being able to express even trivial programs.
[0] https://www.csail.mit.edu/research/synquid-synthesis-liquid-...
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).
I've been thinking lately about how to make this more ergonomic, as I've been getting into lock-free algorithms and would like to be able to specify them nicely in TLA+.
The restriction is a good thing because there are very few humans who can reason about acquire/release semantics in situations other than locks.
I would also note that aside from formal methods, LLMs are absolutely not trustworthy but the top frontier models can reason to some degree about weak memory orderings, and can at least find concurrency bugs which can be later confirmed by human expert review (preferably after eliminating false positives via adversarial LLM review of the findings).
> Atomic variables can be used simply and safely, as long as you are using the sequentially consistent memory model (memory_order_seq_cst), which is the default.
That’s from https://isocpp.github.io/CppCoreGuidelines/CppCoreGuidelines
A lot of companies’ in-house guidelines then say you are allowed to use acquire/release if you are implementing a lock, relaxed if are implementing a counter.
This IMO probably reflects most companies’ distrust in their own developers to develop lock free data structures.
Arguably, seq_cst is helpful for informal reasoning, because it's not hard to imagine all permutations and interleavings. But in my opinion, nobody should be doing lock-free programming based on informal reasoning. Algorithms should be considered incorrect unless they've been rigorously validated, ideally with formal methods or at least model checking.
Very few lock-free algorithms require sequential consistency. There are exceptions, such as Chase-Lev queues, but they are rare.
The added confidence that seq_cst gives you if the algorithm hasn't been properly validated is IMHO worthless.
There's also RustMC for Rust.
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.
I'm not sure there is one, but you can start exploring here:
https://en.wikipedia.org/wiki/Category:Formal_specification_...
For TLA+-styled model checking, though, there is Quint: https://quint.sh/docs/why
I agree that spec/implementation conformance checking is also an issue. P has apparently had some success with PObserve for trace validation (checking whether the log of a running system is a valid execution of a P spec) but it is still not a well-known method with these tools in the same way that fuzzing or property-based testing have become. This requires some real product-level thinking to make usable and possibly full ownership of the system execution environment inside a VM or something like that.
When I write regular TLA+, it's usually for things that aren't nearly as "order-dependent".
As already expressed multiple times, if it isn't like Dafny, Lean, FStar, SPARK, Frama-C, possibly others, where the formal model can be directly mapped to code, I don't see what was actually proven, other than a theoretical exercise.
better question is "what's the markdown of formal modeling?"
the best outcome for everyone is to have something that's so easy it's ubiquitous
> 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
"Three ways formally verified code can go wrong in practice" re: Hoare logic and DbC Design-by-Contract patterns: https://news.ycombinator.com/item?id=45562815
Of course, it still allows the risk that you don't actually get to understand it.
While on the one hand, you do need some kind of grounding in human specification for what to build and what good looks like, any particular defect humans can find should be findable via software.
I’m however pretty sure that if you push a good model hard enough on a code base complex enough it’ll find stuff it wouldn’t have otherwise, the Specula folks have some experience with this.
I think there probably is some value in vibecoding TLA specs and not actually understanding the invariants yourself, but it's way oversold by the talking heads of the tech world, and the gaps need to be filled in some other way if you refuse to write your own code.
The fact is when LLMs get good enough you WILL be able to build software without reading/understanding the code.
Whether or not you think we are already at that point is kind of an unimportant detail.
I would say we are quite close, depending on the type of software you are building.
Good luck with that.
As system complexity continues to increase, tools that are inherently difficult to predict and therefore reason about are unlikely to be the panacea that many today believe them to be.
The internet discovers TLA+. Now what?
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?
A stronger type of reachability property is that a state is always reachable from every other state. This is useful in, for example, eventually-consistent systems where you want to know that your system always could converge to every replica having the same state, even though it never actually does converge unless all writes to the system stop. The article links to a post about how to specify & check those properties in TLA+ (it is possible!) but the way to do this is very much not ergonomic.
Editing to add "there exists a behavior where P is true" is probably meant to mean P is an arbitrary temporal formula. So you are correct that with the limited reachability property you identified, you can express the formula "there exists a behavior satisfying <>S". However, you cannot express anything other than simple formulas like that, not general temporal formulas.
A really good paper on the difference between "possible" and "eventual" is '"Sometime" is sometimes "not never"': https://dl.acm.org/doi/10.1145/567446.567463