We spend a lot of effort making code run and almost none making it argue. An invariant is the cheap proof tool that turns “I think this loop is right” into “I know it is” — and we already use them without naming them.

Tests are a cornerstone of modern development, and somewhere along the way we started treating a green suite as proof. It isn’t: it tells you the cases you thought of still pass, not the ones you didn’t. That confusion was always with us — and it matters more now that an AI agent might be the one chasing the green.