The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Ron wrote:

> Now, it would be very interesting if someone would have formalized all
> x86 instructions or similar. Did anyone do this?
I've formalized in Coq the parts of x86 that I've needed so far for the 
tasks I've attempted.  There is the beginning of a re-usable library for 
parsing machine code (with OCaml) and proving things about the resulting 
ASTs (with Coq) here:
   http://cvs.sourceforge.net/viewcvs.py/proofos/asm/

I know that some other people have also created formalizations, but none 
are really packaged for wide use.  I asked your exact question on this 
list before beginning the above library and received no positive answers.

> Or if not, what is
> the most complex program of which non-trivial statements have been
> proved?
If you count memory safety as non-trivial (and the proofs are quite 
non-trivial!), then we can prove facts about arbitrarily complicated 
programs; anything outputted by a certifying ML compiler, for instance, 
in a format like typed assembly language.  If that's not non-trivial 
enough for you, then probably the Certified Assembly Programming work at 
Yale has dealt with the most interesting properties that I've seen.

> And what software is used most is this context? Coq? With what
> libraries?
>  
Anecdotally, I've heard of the most projects in this area that use Coq.