Yangqing Jia(@jiayq):TLA+ is also (one of the) method that we at Intent Lab used to build mission critical infra software like Agent FS. Key is to make it verifiable and scalable - going through millions of states and also ensure the TLA+ to Rust/C conversion doesn’t weaken the end to end correctness.

2026.09.23 03:54

TLA+ is also (one of the) method that we at Intent Lab used to build mission critical infra software like Agent FS. Key is to make it verifiable and scalable - going through millions of states and also ensure the TLA+ to Rust/C conversion doesn’t weaken the end to end correctness.

Boris Cherny@bcherny

2026.09.22 23:39

I used Opus 5.5 to formally verify the Claude Agent SDK using Lean. A couple short prompts = 16 PRs fixing various bugs and race conditions. Video attached. TLA+ also works well. I sometimes combine Lean and TLA+ to look for issues around data flow, concurrency, and state mgmt. I don't know either language well, but Claude is excellent at both. This approach is super useful for formally modeling your code and finding bugs that a human probably wouldn't have spotted. Is formal verification the future of coding (or at least, bug finding)?