Hacker News new | ask | show | jobs
by atomicnature 34 days ago
Just a question to people who may know better than me about this.

I thought the whole point of trying to write out TLA+ is so that you get a better idea of what you want and put it into formal language?

I get that an LLM can assist/help with expressing what we want in formal language a bit, but if one automates all this there is no human intent/design anymore.

If the LLM generates both the design (TLA+) and writes an arbitrary program that satisfies said design -- what exactly have we proved?

What assurance do humans get since human doesn't know or cannot specify what they want.
1 comments
majormajor 34 days ago
An LLM-generated TLA+ model can be verified for certain things in a way that LLM-generated code can't. It's infamously hard to exhaustively unit-test concurrency.

Whether or not you're modeling the right things or verifying the right things, of course... that's always left as an exercise for the user. ;)

(How to prove the implementation code is guaranteed to match the spec is a trick I haven't seen generalized yet, either, too.)

link
kiwicopple 34 days ago
> It's infamously hard to exhaustively unit-test concurrency.

a useful example from last week where TLA+ found a bug in pg_rewind:

https://multigres.com/blog/2026/05/04/tla-pg-rewind

link