Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Can LLMs model real-world systems in TLA+?

sigops.org

Post reply on HN
Print view View original

21–30 of 40 posts

Re: Can LLMs model real-world systems in TLA+?

#21

Post by iFire »

dmos62 wrote: post #20
iFire wrote: post #8

I don't use tla+ to model real-world systems anymore, Claude is able to model systems in Lean 4 and the binary executable can handle real input or I can directly generate c / rust on proofs with numeric types that have ring structure (integers, rationals, bits). https://github.com/lambdaclass/truth_research_zk

Do you find Lean 4 sufficient for highly async systems?

I haven't made money on yet, but I'm trying to model a webtransport (http/3, quic) system for massive multiplay vr games.

See https://aws.amazon.com/builders-library/challenges-with-dist... for how async related to distributed systems.

Re: Can LLMs model real-world systems in TLA+?

#22

Post by NooneAtAll3 »

tombert wrote: post #7

Claude has certainly been getting better with TLA+. It's not perfect yet but for laughs I got it to model the rules of Monopoly last night [1]. I haven't done any exhaustive checking on it yet, but it certainly looks passable. It is pretty impressive at how good it's gotten at this, in a relatively short amount of time no less. I still usually write my specs by hand, but who knows how much longer I'll be doing that.…

> I haven't done any exhaustive checking on it yet, but it certainly looks passable.

isn't that exactly the kind of fails LLMs do the most? first-glance-passable nonsense?

Re: Can LLMs model real-world systems in TLA+?

#23

Post by NooneAtAll3 »

thomasahle wrote: post #15
iFire wrote: post #8

I don't use tla+ to model real-world systems anymore, Claude is able to model systems in Lean 4 and the binary executable can handle real input or I can directly generate c / rust on proofs with numeric types that have ring structure (integers, rationals, bits). https://github.com/lambdaclass/truth_research_zk

I'm currently choosing between the right formalization for a big hardware project. I'm considering between SVA, TLA+ and Lean. With the former being more domain specific and the later more general. Do you think we'll move towards "Lean for everything" or do domain specific formalisms still make sense?

what's SVA?

Re: Can LLMs model real-world systems in TLA+?

#25

Post by IshKebab »

NooneAtAll3 wrote: post #23
thomasahle wrote: post #15

Earlier quoted context omitted.

I'm currently choosing between the right formalization for a big hardware project. I'm considering between SVA, TLA+ and Lean. With the former being more domain specific and the later more general. Do you think we'll move towards "Lean for everything" or do domain specific formalisms still make sense?

what's SVA?

SystemVerilog Assertions. Hardware (silicon ASICs, and also FPGAs often) are written in a language called SystemVerilog. It has a feature called "concurrent assertions" which is usually just called SVA.

These are sort of temporal regexes, e.g. you can write

  assert property($fell(rst) |-> foo == 1 ##[1:20] foo == 0)
Which means if the rst signal fell (changed to 0) then foo must be 1 and 1-20 cycles later it must be 0.

The nice thing about them is that there are a few commercial tools that can formally verify them. They're super expensive (~$100k/year for one license), but fairly widely used because they work really well.

It's probably the most successful application of formal verification because it doesn't require much expertise to use. Unlike software formal verification which pretty much immediately requires you to become an expert on loop invariants, termination measures, hoare triples etc. At least that has been my experience.

Re: Can LLMs model real-world systems in TLA+?

#26

Post by randusername »

tombert wrote: post #7

Claude has certainly been getting better with TLA+. It's not perfect yet but for laughs I got it to model the rules of Monopoly last night [1]. I haven't done any exhaustive checking on it yet, but it certainly looks passable. It is pretty impressive at how good it's gotten at this, in a relatively short amount of time no less. I still usually write my specs by hand, but who knows how much longer I'll be doing that.…

What's the advantage of provable correctness if it's apparently not easy to prove even for people who understand TLA+? I'm not trying to be a party pooper, just curious.

Isn't logical incorrectness less of a problem in software than failures of imagination or conscientiousness in modeling the domain?

Re: Can LLMs model real-world systems in TLA+?

#28

Post by kiwicopple »

majormajor wrote: post #14
atomicnature wrote: post #12

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…

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, e…

> 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

Re: Can LLMs model real-world systems in TLA+?

#29

Post by kown7 »

thomasahle wrote: post #15
iFire wrote: post #8

I don't use tla+ to model real-world systems anymore, Claude is able to model systems in Lean 4 and the binary executable can handle real input or I can directly generate c / rust on proofs with numeric types that have ring structure (integers, rationals, bits). https://github.com/lambdaclass/truth_research_zk

I'm currently choosing between the right formalization for a big hardware project. I'm considering between SVA, TLA+ and Lean. With the former being more domain specific and the later more general. Do you think we'll move towards "Lean for everything" or do domain specific formalisms still make sense?

Have you considered P? It feels like a good abstraction for engineers as it's "proper" code.

https://github.com/p-org/P

Re: Can LLMs model real-world systems in TLA+?

#30

Post by tclancy »

randusername wrote: post #26
tombert wrote: post #7

Claude has certainly been getting better with TLA+. It's not perfect yet but for laughs I got it to model the rules of Monopoly last night [1]. I haven't done any exhaustive checking on it yet, but it certainly looks passable. It is pretty impressive at how good it's gotten at this, in a relatively short amount of time no less. I still usually write my specs by hand, but who knows how much longer I'll be doing that.…

What's the advantage of provable correctness if it's apparently not easy to prove even for people who understand TLA+? I'm not trying to be a party pooper, just curious. Isn't logical incorrectness less of a problem in software than failures of imagination or conscientiousness in modeling the domain?

My thought (as someone interested in formal verification but unable to grok the math) is it exists as a canary in any sufficiently-complex codebase I let AI create. Even if it's wrong, knowing that something "we" changed breaks an agreement things currently assume is valuable.
Post reply on HN