Thread

What TLA+ can and can't check

243 points · 51 comments · b-man

Loading the complete thread in the background. This saved snapshot is available now. Refresh

adamddev1 · 1790787121 · focus · HN ↗
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.
1. _flux · 1790792883 · focus · HN ↗
  These probabilistic guessing machines are pretty great for creating these formal models, e.g. TLA+, and then guessing if the implementation aligns with the spec.. In fact, it's my go-to tool for constructing soft guardrails for the model, so the design it's going to implement is logically sound. Same as for people: it's easier to make something working when you have a spec that is working.
  Of course, it still allows the risk that you don't actually get to understand it.
2. jldugger · 1790793117 · focus · HN ↗
  > People can't escape the need to actually understand the things they are building.
  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.
3. nonethewiser · 1790797465 · focus · HN ↗
  I wonder if asking an LLM to model their implementation in TLA+ first would improve their implementations.
  1. baq · 1790800056 · focus · HN ↗
    It does somewhat, or at least used to for a few months. Nowadays it kinda seems that the models have internalized something like TLA and are thinking in it in parallel to thinking in the language they’re writing, so it doesn’t help as much. This is all educated guesses from me, I’ve been telling models to do TLA back in the stone age around February.
    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.
    <a href="https://github.com/specula-org/Specula" rel="nofollow">https://github.com/specula-org/Specula
  2. senderista · 1790800147 · focus · HN ↗
    A TLA+ spec defines both a model and properties (global invariants). How do you know that the properties the LLM specifies are the ones you care about?
    nonethewiser · 1790819215 · focus · HN ↗
    My question is concerned with improving quality of AI implementations. Its plainly true, uninteresting, and beside the point to observe that AI cannot read minds.
4. rozap · 1790800896 · focus · HN ↗
  I recently had this discussion with an energetic junior coworker who just learned about TLA+ and thought it would solve all the problems. I think it probably did give the LLM that he was using to do the actual implementation a better starting off point, but the obvious gap remains, which is whether or not the spec (TLA) matches the implementation (elixir) which there's just not a good answer for. I encouraged him to put his TLA code in our docs folder, because as far as I'm concerned, it's just a suggestion, and then write (and understand...) some property tests about the feature.
  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.
  1. theknarf · 1790941174 · focus · HN ↗
    <a href="https://www.youtube.com/watch?v=ovlQ81rBc-4" rel="nofollow">https://www.youtube.com/watch?v=ovlQ81rBc-4
5. IshKebab · 1790801801 · focus · HN ↗
  How do managers build software?
  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.
  1. Revanche1367 · 1790854901 · focus · HN ↗
    Are you not implying that SWEs are the same as probabilistic guessing machines by analogizing the LLM-user with a human developer’s manager?
  2. __alexs · 1790861383 · focus · HN ↗
    Manager's do not build anything despite what the management-class might want you to believe.
  3. jasomill · 1791053433 · focus · HN ↗
    This is like saying that computers will get fast enough and compilers will be good enough at catching mistakes that you won't need to care about performance or correctness.
    Good luck with that.
6. panarky · 1790817981 · focus · HN ↗
  Speaking as a probabilistic guessing machine who tries to actually understand the thing I'm building, this approach hasn't proven foolproof either.
rrook · 1790788902 · focus · HN ↗
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.
1. bunderbunder · 1790791692 · focus · HN ↗
  I don't think you're envisioning quite the same thing, but what you say reminds me of the "Von Neumann Languages Lack Useful Mathematical Properties" section in John Backus's Turing award paper. One of his criticisms of what we would now call imperative languages is that they make it exceedingly difficult to formally prove facts about a program.
  <a href="https://dl.acm.org/doi/epdf/10.1145/359576.359579" rel="nofollow">https://dl.acm.org/doi/epdf/10.1145/359576.359579
sourdecor · 1790788919 · focus · HN ↗
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]: <a href="https://github.com/quint-co/quint" rel="nofollow">https://github.com/quint-co/quint
[1]: <a href="https://news.ycombinator.com/item?id=49865720">https://news.ycombinator.com/item?id=49865720
ChrisArchitect · 1790789884 · focus · HN ↗
Related:
The internet discovers TLA+. Now what?
<a href="https://news.ycombinator.com/item?id=49863600">https://news.ycombinator.com/item?id=49863600
westurner · 1790791275 · focus · HN ↗
From "How did software get so reliable without proof? (1996) [pdf]" <a href="https://news.ycombinator.com/item?id=42425617">https://news.ycombinator.com/item?id=42425617 :
> From "The Future of TLA+ [pdf]" (2024) <a href="https://news.ycombinator.com/item?id=41385141">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
1. grohan · 1790863677 · focus · HN ↗
  I quite enjoyed Tony Hoare's essay - thanks for sharing. A lot of what he wrote has stood the test of time!
  1. westurner · 1790912027 · focus · HN ↗
    Re: Hoare logic; Precondition, Command, Postcondition: <a href="https://news.ycombinator.com/item?id=47335703">https://news.ycombinator.com/item?id=47335703
    "Three ways formally verified code can go wrong in practice" re: Hoare logic and DbC Design-by-Contract patterns: <a href="https://news.ycombinator.com/item?id=45562815">https://news.ycombinator.com/item?id=45562815
singron · 1790792099 · focus · HN ↗
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).
1. ahelwer · 1790793919 · focus · HN ↗
  This is true, and it falls into the "possible but not ergonomic" category for modeling systems like this in TLA+. Concurrent programs reading & writing to shared variables can be reordered at two levels: the compiler, and then the CPU. Specifying this in TLA+ is possible but difficult, and your conventional TLA+ specification will assume things happen in a linear order within each thread, and are interleaved arbitrarily between threads. In other words by default PlusCal works like there is both a barrier and memory fence between each action. Even with strong memory semantics like x86-TSO, specifying something like the action of the store buffer (where a core writes a value and can read the updated value but its write is not yet visible to other cores) requires actually writing your own tiny implementation of x86-TSO; there isn't one already defined as a library you can easily use.
  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+.
2. kccqzy · 1790796537 · focus · HN ↗
  [delayed]
  1. senderista · 1790799889 · focus · HN ↗
    Which style guides? That makes no sense to me because 1) if you're writing a lock-free algorithm/data structure you presumably both know what you're doing and care a lot about performance, 2) many lock-free algorithms don't even require any seq_cst operations (or equivalent fences), and 3) weak memory orderings can be essential to getting acceptable performance in critical paths.
    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).
    kccqzy · 1790800559 · focus · HN ↗
    The well-known C++ Core Guidelines say this:
    > 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 <a href="https://isocpp.github.io/CppCoreGuidelines/CppCoreGuidelines" rel="nofollow">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.
    raphlinus · 1790817323 · focus · HN ↗
    I disagree with this advice, and consider it outdated.
    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.
    kccqzy · 1790822253 · focus · HN ↗
    I disagree as well. It’s more of a clutch to make inexperienced people complain that their lockless algorithm is slow and find a reputable third-party library instead.
    senderista · 1790830798 · focus · HN ↗
    Agree, look at how many incorrect concurrent algorithms have been published over the years, where seq_cst is assumed. It's easy enough to mess up concurrency without any weak memory orderings. There are only a few people I know of who I would trust to informally reason about weak memory orderings in nontrival algorithms (Dmitry Vyukov, for one).
3. hansvm · 1790800099 · focus · HN ↗
  Yeah, the last time I had to check anything regarding memory orderings, I wrote a custom analyzer for that problem. It's...not easy. The state space is enormous too, so even with compiled code I had to take some shortcuts and prove parts of the problem by hand.
4. anonymousDan · 1790808808 · focus · HN ↗
  For C++ GenMC is probably the state of the art for this: <a href="https://plv.mpi-sws.org/genmc/" rel="nofollow">https://plv.mpi-sws.org/genmc/
  There's also RustMC for Rust.
kylegalbraith · 1790794313 · focus · HN ↗
[dead]
lou1306 · 1790797916 · focus · HN ↗
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?
1. ahelwer · 1790798266 · focus · HN ↗
  You are quite close! That does indeed encode a limited form of reachability property - that P is reachable from at least one start state. As the article mentioned, these kinds of reachability properties are now actually available for TLC to check without having to jump through the hoop of negating it first.
  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.
  1. hwayne · 1790798711 · focus · HN ↗
    On top of what Andrew said, "failure as reachability" is a property of the implementing model checker, not the formalism itself! If you convert "we can win the game" to "it's not true that always we haven't won" and write that up as a TLA+ formula, you get `![](!won)". But that means "we win in every behavior", aka `<>won`!
    A really good paper on the difference between "possible" and "eventual" is '"Sometime" is sometimes "not never"': <a href="https://dl.acm.org/doi/10.1145/567446.567463" rel="nofollow">https://dl.acm.org/doi/10.1145/567446.567463
  2. lou1306 · 1790837866 · focus · HN ↗
    Yeah I see now that P in the original post means a _property_, not a _predicate_. That clears it up :)
IshKebab · 1790802004 · focus · HN ↗
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.
1. Jtsummers · 1790803492 · focus · HN ↗
  [delayed]
2. ahelwer · 1790803519 · focus · HN ↗
  It's a reasonable question. There are novel things I like about the syntax - like vertically-aligned conjunction & disjunction lists - but I don't really want to defend syntax that still uses all-caps KEYWORDS like it's the COBOL era and makes you use string values for enums. The underlying formalism is, however, amazing for thinking in, and it's used by P, Quint, and FizBee which all to varying degrees paint themselves as TLA+ successor languages.
  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.
3. tombert · 1790804995 · focus · HN ↗
  I feel like PlusCal and TLA+ operate at a different level. I use PlusCal primarily when what I'm modeling has a lot of sequential "A then B then C..." steps. With PlusCal a program counter is implied and it maps more directly to sequential algorithms.
  When I write regular TLA+, it's usually for things that aren't nearly as "order-dependent".
4. beu5a · 1790806070 · focus · HN ↗
  You should look into Quint: <a href="https://github.com/quint-co/quint" rel="nofollow">https://github.com/quint-co/quint. It comes with simple syntax and very good developer tooling. Quint to TLA+ is what Typst is to Latex.
5. pjmlp · 1790838107 · focus · HN ↗
  I like how PlusCal looks, however I vouch for the same sentiment as you.
  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.
  1. ahelwer · 1790866245 · focus · HN ↗
    Many TLA+ users will tell you the greatest value of writing a spec was it forced them to think clearly about their system. However, thinking is very hard to sell, so we tend to center the razzle-dazzle about model-checking properties of your state space. Which is a great capability, don't get me wrong! Most non-trivial systems have a state space far larger than can be assessed for finding bugs via thinking.
6. NooneAtAll3 · 1790840081 · focus · HN ↗
  > What is the Typst of formal modeling?
  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
  1. Revanche1367 · 1790855785 · focus · HN ↗
    The closest thing I’ve come across to this is Z (“Zed”) notation. It’s from the 80s, quite influential and pretty easy to read with a bit of logic symbolism. The same designer (Jean-Raymond Abrial) and colleagues also made the B method which can also do program refinement. Several other “well-known” (relative to other formal methods) formal specification systems were influenced by Z, including possibly TLA+ as I’ve read somewhere (but cannot confirm). Z and B both have free tooling available online.
metabagel · 1790804929 · focus · HN ↗
Love the inline footnotes!
maxgashkov · 1790825298 · focus · HN ↗
Do we need... TLA++?
codedump · 1790827822 · focus · HN ↗
[dead]
spaintech · 1790832963 · focus · HN ↗
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.
1. pjmlp · 1790837910 · focus · HN ↗
  Ada/Spark don't tend to be much used in the startup circles influenced by SV culture.
  You have to go into high integrity computing industry and related conferences to see it being used.
2. agentultra · 1790858945 · focus · HN ↗
  I’ve toyed around with parsing the TLA+ spec and generating property based test assertions from the invariants.
  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] <a href="https://www.csail.mit.edu/research/synquid-synthesis-liquid-types" rel="nofollow">https://www.csail.mit.edu/research/synquid-synthesis-liquid-...
Revanche1367 · 1790837705 · focus · HN ↗
I've been trying to get into formal specification & verification too, but with Z notation (which is specifically for specification) instead, together with a couple of different theorem-provers. It's for a pet project to help me learn, so not something I would be using for serious work (not right away at least), but I find the Z notation quite readable and there is quite a bit support and free tooling for it available online. Being quite new to formal methods, I think TLA+ would be overkill for learning.
<a href="https://en.wikipedia.org/wiki/Z_notation" rel="nofollow">https://en.wikipedia.org/wiki/Z_notation
1. jz391 · 1791117611 · focus · HN ↗
  You mentioned good tools available for Z - do you have any recommendations? I have tried in the past using VDM (alternative to Z, similar level) for writing down specifications precisely, but could never find adequate tools for maintaining/checking proofs/derivations.
luca_checkdesk · 1790840988 · focus · HN ↗
[dead]
TachyonProducti · 1790850173 · focus · HN ↗
[dead]
GnosiWorks · 1790851578 · focus · HN ↗
[dead]
chelseahermes · 1790863357 · focus · HN ↗
[dead]
haroldopina · 1790863526 · focus · HN ↗
[dead]

Open on Hacker News to reply ↗

Unofficial Hacker News client; not affiliated with Y Combinator.