People assume that in an AI doing formal verification world, they can take their existing codebase, ask AI to prove it correct, and get either a proof or a bug. Sadly reality has a few bones to pick with this, and one of them is the "existing codebase" part. And that's due to
Existing codebases block AI formal verification
Hillel Wayne argues that handing a legacy codebase to AI won't simply yield a proof or a bug: the codebase itself often lacks the preconditions formal verification requires.