Verdict
Yes
Yes, write tests for code you proved correct by hand: one test per case of the proof and one per assumption it makes, such as sorted input or a sum that fits in an int, because the proof covers only the code as it was when you proved it.
Why
- Blast radiususers
- Change frequencyrarely
- Detectabilityeventually
- Reversibilitywith-effort
- Test costtrivial
Yes, write tests for code you proved correct by hand, one per case of the proof and one per assumption it makes. For the typical case, a calendar's free-slot finder proved on paper with no tool checking the proof, Blast radius is users and Change frequency is rarely, and each change voids the proof. Detectability is eventually, because a wrong result such as a missed slot looks plausible. Reversibility is with effort, because other code stores the result, and Test cost is trivial, because the proof already lists the cases; rule R11 gives Test.
| When | Decision | Why |
|---|---|---|
| The proved function prorates a subscription charge after a plan change | Test mandatory: the first and last day of the period, and an amount that does not divide evenly | Blast radius rises to money and Reversibility to costly: a wrong charge ends in refunds |
| A verifier such as Dafny checks the proof on every build and blocks the merge, and a second person reviewed the specification | Do not test what the verifier proves; test the unverified code around it, such as input parsing | Detectability moves to immediately and Reversibility to trivial: a change that breaks the proof never merges |
| The proved function checks its own result before returning, such as `a[i] == key` after a search, and raises an error | Test minimally: one test of the main path, and keep the check in production code | Detectability moves to same-day and Reversibility to trivial: a wrong result becomes a reported error that stores nothing |
| The proof covers a replication protocol whose failures need message orders that no local setup reproduces | Test it differently: a production job checks the proved invariant across replicas and alerts on a difference | Test cost rises to heavy, while Detectability stays eventually and Reversibility with-effort |
| The proved code is a migration that runs once | Test it differently: run the migration on a copy of the data and compare row counts | Change frequency falls to once: a test in the suite would never run again |
What breaks if you don't test
Six months after your proof, a colleague adds a 15-minute buffer between meetings to the free-slot finder and gets the boundary wrong; nobody rechecks your notes. The finder offers slots that overlap the next meeting, customers book them, and support hears about it weeks later, when two people arrive for one slot. The proof can also fail with no edit: it assumed sorted busy intervals, and a new caller passes them unsorted.
What you lose if you over-test
The proof already gives you the case split, so examples beyond it repeat work. Tests that assert intermediate steps, such as a loop cursor, fail on every refactor that keeps the result. Hand-picked examples also give false confidence: people pick small numbers and miss an overflow near Integer.MAX_VALUE.
How to test
Write unit tests from the proof: one per case, such as the empty input, one element and the boundary where the invariant starts, and one per assumption, such as unsorted input and the largest integer. Add one property-based test that states the proved claim, such as "no free slot overlaps a busy interval", and let jqwik or Hypothesis generate inputs in CI. For a small input domain, such as every 16-bit value, test every input. To have a tool check the proof on every build, write the function in Dafny and test the glue around it. A runtime check must raise an error explicitly: Python drops assert under -O.
When the answer changes
- A verifier checks the proof on every build, and a second person reviewed the specification.
- The function computes money or decides who can see a record.
- The code runs once, as a migration does.
Real incident + Code example
The binary search that was proved correct
Jon Bentley proved a binary search correct in Programming Pearls, and it had an overflow bug. Joshua Bloch's binary search in the JDK had the same bug, and in 2006 he reported that it fails for arrays of 2^30 elements or more, after about nine years in the JDK. The proof treated low + high as a mathematical integer; a Java int has 32 bits:
static int midpoint(int low, int high) {
return (low + high) / 2; // proved correct, overflows above 2^31 - 1
}
@Test
void midpointOfLargeIndexes() {
assertEquals(1_550_000_000, midpoint(1_500_000_000, 1_600_000_000));
// fails: the sum wraps around, and midpoint returns -597483648
}
The test needs no billion-element array, because it checks the proof's assumption about integer width. The fix is low + (high - low) / 2. Bloch's conclusion: "It is not sufficient merely to prove a program correct; you have to test it too."
Related questions
FAQ
- Should I write tests when I can prove code correctness?
Yes, write tests for code you can prove correct, because the proof covers the code on the day you wrote it and tests check every later change in CI. Donald Knuth ended a 1977 memo with "Beware of bugs in the above code; I have only proved it correct, not tried it."
- Does formal verification replace unit tests?
No, formal verification replaces unit tests only for the properties the verifier checks on every build. The Csmith fuzzer found six wrong-code bugs in the unverified front end of the verified C compiler CompCert, and none in a later version after about six CPU-years of testing.
- Can tests prove that code is correct?
No, a test shows that code works for the inputs it runs. An exhaustive test over a small domain, such as every 16-bit value, is a proof.
- What should I test in code I have proved correct?
Test each case the proof splits into and each assumption it makes, such as sorted input, a sum that fits in an int, or exact decimal arithmetic. A proof on paper takes each of these as given.