x-bcherny-lean-agent-sdk

Extract — Cherny X: Lean/TLA+ on Claude Agent SDK (buzz vs clarification)

• URLs:
  • Claim: https://x.com/bcherny/status/2102543349102338309
  • Clarification: https://x.com/bcherny/status/2102803868837126172
• Author: Boris Cherny (@bcherny) — Claude Code @ Anthropic
• Read via: user-X get_posts_by_ids (note_tweet full text)
• Times (CST/Asia Shanghai): claim 2026-09-23 07:39 CST; clarification 2026-09-24 00:54 CST

Claims (2102543349102338309)

• Used Opus 5.5 to “formally verify” the Claude Agent SDK with Lean; “a couple short prompts” → 16 PRs fixing bugs and race conditions (video attached).
• TLA+ also works; sometimes combine Lean + TLA+ for data flow, concurrency, state management.
• Author does not know either language well; Claude is excellent at both.
• Framing: “super useful for formally modeling your code and finding bugs”; ends with “Is formal verification the future of coding (or at least, bug finding)?”
• Engagement (at fetch): ~1.97M impressions, 5654 likes, 482 replies, 322 reposts, 290 quotes — viral buzz post.

Clarification (2102803868837126172)

Reply to @0x9212ce55 (who argued “larping” FV / no magic wand to prove no bugs):

“Verify” is a little loose yeah. In practice, it has been pretty useful for Claude to do something like:

1. Build a model of the program, targeting a tricky state machine or race-prone part
2. Find counter-examples in the model: these are suspected bugs
3. Reproduce the bugs
4. Fix the bugs

So the operational loop is model → CEx → reproduce → fix, not product-level end-to-end FV of the shipped SDK.

DIY / fleet relevance

• Treat Cherny-style Lean/TLA+ agent use as high-value bugfinding via models, not as a substitute for kernel-checked product proofs.
• Useful DIY pattern: constrain agent to race/state-machine slices; require CEx reproduction before merge.
• Brief question “Where do agent+FV claims overreach?” — this thread is the canonical overreach→clarification example.
• Pair with RV Inc response (same conversation cluster) for industry framing of model≠runtime.

Caveats

• No public Lean/TLA+ artifacts or proof logs linked in the posts.
• “16 PRs” / race fixes are author-reported; no independent audit in-thread.
• Video not transcribed here.