TLA+
System softwareWikipedia
23
MENTIONS
4
EPISODES
4
PODCASTS
Search complete. 23 mentions across 4 episodes found for "TLA+".
Sep 8, 2026
Ryan DonovanHOST
LLMs are not graded numbers, right? Yes.
Ryan DonovanHOST
Something I've heard recently is using proving languages, like Lean or TLA+.
Ryan DonovanHOST
Do you do any sort of validation through that?
Srini VenkatesanGUEST
Not right now.
JamieHOST
They're a timeline problem for infrastructure teams tracking how fast they patch.
JamieHOST
In the harness, tools, and orchestration world, Dan Lu ran coding agents through twenty-six different prompt conditions, roughly eighty runs each, all building the same Zstd compressor under instructions ranging from a bare default to test-driven development, property-based testing, and formal methods tooling like TLA+ and Lean4.
JamieHOST
The default instructions beat most of the supposedly rigorous conditions outright.
JamieHOST
Test-driven development actually produced worse tests that missed edge cases the default approach caught, and of eighty runs told to use TLA+, only five agents actually wrote the formal spec before writing code.
JamieHOST
The failure mode is mimicry.
JamieHOST
Agents copy a technique's syntax without performing its substance.
David WynnHOST
Jesse talks about MongoDB's journey with formal verification, as well as his own.
David WynnHOST
He shares what it was like to build a custom replication protocol using TLA+, and how he realized that you can work in TLA+, without a PhD.
David WynnHOST
Jesse and Carl also talk about the future of formal methods, the impact of AI, the advent of simple but powerful tools like Antithesis, and Jesse's predictions about the future of code review.
David WynnHOST
You'll want to stick around.
Jesse Jiryu DavisGUEST
We were one of the first, actually.
Jesse Jiryu DavisGUEST
And we actually built that system before Raft had been published in 2014.
Jesse Jiryu DavisGUEST
And it was a home-built system that worked pretty well, but It wasn't designed with any sort of formal logic like TLA+, and it had some bugs like
Carl SverreHOST
it showed.
Chris FordGUEST
You might also have a finite state machine that reflects where you want the payment processing logic.
Chris FordGUEST
even have something as fancy as TLA+, which is this modeling tool that's kind of popular in kind of hipster nerd circles, you might have various different representations of the truth.
Chris FordGUEST
And it's my belief that the Swiss cheese model of quality applies here.
Chris FordGUEST
So the Swiss cheese model of quality is, I've gotten and use it in aviation a lot.
9 MINS LATER
Henry GarnerHOST
I can't say I've seen anybody actually fully committing to that way of working
Chris FordGUEST
yet.
Henry GarnerHOST
But presumably, well, and it's linked to the point you made about, I think it was nerds and TLA plus.
Chris FordGUEST
Yeah.