AI proved your code correct. What did it actually prove?

Keller AI explains how formal verification works, using a sorting example and Euclid's equilateral-triangle construction to show how proofs combine definitions, assumptions and prior results, then applies the approach to a document-download authorization handler. The article stresses that a checked proof only establishes a result within a mathematical model, so its value depends on whether the model's assumptions match reality and whether the specification captures the intended requirement, citing a revocation-versus-session example and timing side channels. It also reports an unreproduced synthetic experiment in which the best of seven automated reviewer setups approved 1 of 88 sealed rule-breaking changes.