“Proof requires us to understand why it works.”
The sort algorithm from a 2021 paper looks wrong and works anyway. SPARK and Z3 proved it for small arrays by unrolling loops, then fell over until a human wrote correct loop invariants and found an off-by-one. The final proof still skips showing the output is a permutation of the input. Formal verification is real, and it still runs on human judgment.