The Coq mailing list

[Tom Ridge <tjr22 AT cam.ac.uk>]

Dear All,

I am interested in substantial, state-of-the-art examples of program
verification. "Program" should be interpreted quite widely, e.g. so as
to include Gonthier's four-colour theorem work, and Harrison's HOL in
HOL work. "Verification" should also be loosely interpreted, to include
very weak properties such as e.g. absence of null-pointer dereference,
as well as strong properties such as functional correctness, liveness etc.

I would be very grateful if people could reply to this message with
their favourite examples.

I will attempt to set up a wikipedia page with the information so gleaned.

Many thanks

Tom