[SystemSafety] 7% of mistakes in Coq proofs go undetected

[Derek M Jones]

All,

Some interesting results from the mutation analysis of Coq proofs:
http://cozy.ece.utexas.edu/mcoq/

Mutation analysis introduces a mistake into code, by mutating existing
code at some point (there is a small cottage industry working on new
mutation operators), and the modified code is executed in some way.

A common research use (not much used in industry) is using mutated
code to check the quality of a test suite, i.e., a thorough test
suite will detect the added mistake.

"Mutation Analysis for Coq" does what it says on the tin.  It mutates
Coq proofs, and then checks whether the verification fails (which it
should do).

In 7% of cases (6.82% to be exact), verification succeeded (averaged
over all mutations).

So, those of you who have paid for Coq proofs to be written for your
software.  If the proof contains a mistake, there is something like
a 7% chance it has gone undetected.

Do companies offering "proofs of correctness" provide fix-it for free
guarantees?  Or do the claims of correctness never make it from the
marketing department to a signed contract?

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com