Boris Cherny
@bcherny
More details for the formal methods people -- what's happening is Claude is doing something like:
1. Building a model of the program, targeting a tricky state machine or race-prone part of the code
2. Finding counter-examples in the model. These are suspected bugs
3. Reproducing the bugs
4. Fixing the bugs in the code
It's not that the whole codebase is formally verified (yet!..), more that the hairiest parts of the code are modeled, checked for counter-examples, and fixed.
