[Cryptography] The Case for Formal Verification

Derek Jones derek at knosof.co.uk
Thu Sep 19 06:33:09 EDT 2013

Perry E. Metzger <perry <at> piermont.com> writes:

> CompCert is a fine counterexample, a formally verified C compiler:
> http://compcert.inria.fr/
> It works by having a formal spec for C, and a formal spec for the
> machine language output. The theorem they prove is that the

The claim of CompCert being a formally verified C compiler is wildly overstated:

It is a good start, but they still have lots of work to do.

More information about the cryptography mailing list