Boris Cherny shares prompts for formally verifying Claude Agent SDK

Boris Cherny says he used Opus 5.5 with Lean to formally verify the Claude Agent SDK, with a couple of short prompts producing 16 PRs fixing bugs and race conditions. He also reports that TLA+ works well, sometimes combined with Lean to find data flow, concurrency, and state management issues. The post links to his actual prompts as another example.