Product

Testing vs. verification.

A test checks the inputs someone wrote down. A proof checks every input. Three things change about how software gets built.

What it covers

With testingThe inputs someone wrote, or a fuzzer happened to try.

With TheoremEvery input the specification describes.

With testingTests of internals are ported or rewritten; the gaps have to be found again.

With TheoremThe same specification; the proof is redone and machine-checked.

With testingA new edge case is caught only if it is sampled.

With TheoremCovered: the specification already says what every input must do.

With testingEach change, and the tests that come with it.

With TheoremThe specification, once. A change that still satisfies it needs no further review.

A specification your engineers can readThe property, in a few lines, against what the code must do.
A proof checked by a machineA proof assistant checks it. You trust the checker, not our models.
Every bug on the wayAnything that would break the property surfaces first.
The proof again, on every changeEach build gets a new proof, in your pipeline, where a test would run.
Evidence for the people who askAn artifact that says the property holds, for auditors, customers and procurement.