The proof was valid. The theorem was the wrong one

The task looked clean: prove that a widely used C library round-trips JSON, that taking a value, writing it out, and reading it back returns the same value. It is the kind of property a formal proof is made for, precise and total. The honest outcome was that the theorem is false of the library, and that no amount of proving effort could have made it true.

The reason is in the library’s own number handling. It prints numbers with limited precision, reads them back, and only reaches for more digits when the re-read “differs”, where “differs” is judged by a tolerance, not by equality. So writing a number and reading it again can quietly change it. Round-tripping is not a property the library has. It is not a difficulty to be worked around; it is simply absent.

Here is where a proof turns dangerous. Faced with a target that lacks the property, the locally rational move is to weaken the statement until it goes through: restrict to small numbers, add an approximation hypothesis, prove round-trip up to a tolerance. Each of those compiles. Each produces a green build and a theorem that is true. And each certifies nothing about the property anyone actually wanted. The proof would be valid; the theorem would be the wrong one; and a reader glancing at “round-trip: proved” would take away exactly the assurance that was not there.

What breaks the trap is not more proving but validating the specification against the target before proving anything, checking, on known cases, that the property stated is the property meant. Do that here and the round-trip statement is exposed as false of the library on contact, before any effort is sunk into proving a weakened cousin. The resolution the artifact took was to model numbers exactly rather than as machine floats, which makes an honest round-trip theorem both true and provable, and turns every divergence from the C into a measured finding rather than a hidden defect.

This is the faithfulness failure in its clearest form: the formalism states a property, and it is not the one intended, so the proof is valid and the theorem is wrong. It is the sharpest of the failures the programme catalogues, because it is the one where every internal signal, the build, the kernel, the absence of gaps, says success while the thing that mattered was never checked.

This case is the formal-verification corner of a programme about whether claims about AI systems can be independently checked. Read where it fits in the programme.