Formal verification in commercial software: a field report
We applied formal methods to a payment reconciliation engine. It found four bugs that eleven thousand tests had missed. Notes from the frontier of verified software.
Formal verification has a reputation: academically beautiful, commercially irrelevant. After applying it to a production payment reconciliation engine, we disagree — with caveats.
The engine had eleven thousand tests and a clean two-year incident history. Model-checking its core state machine still surfaced four latent defects, each requiring a precise interleaving of retries and partial failures that no test had constructed and production had simply not yet rolled.
The caveat is scope. Verifying the whole system would have been economically absurd; verifying the two hundred lines where the money moves took three weeks and paid for itself on the first finding. That is the pattern we now recommend: formal methods as a scalpel, applied exactly where failure is unaffordable.
