Twelve days of TLA+ on my own tools

On 22 September Boris Cherny, who created Claude Code, wrote on X that he had used Opus 5.5 to formally verify the Claude Agent SDK with Lean. Further down his post he added, "TLA+ also works well. I