This project has moved and is read-only. For the latest updates, please go here.

Welcome to x86proved

x86proved is a Coq library that supports modelling, specification, generation, and proof for x86 machine code programs.


To use x86proved you will need
  • The Coq proof assistant, version 8.4
  • The ssreflect tactic language and library, version 1.4
  • A Coq development environment such as CoqIDE or emacs + Proof General
You can obtain all three bundled for 32-bit and 64-bit Windows from Pierre-Yves Strub's web page.
You will need either
  • On Windows: nmake.exe, supplied with Visual Studio, versions of which you can download for free
  • On Unix/Cygwin: make


Under construction


There are many ways to contribute to x86proved.
  • Extend the model to cover more features of x86 e.g. instructions, floating point, 64-bit, SIMD, paging, multi-core
  • Improve the automation of proofs
  • Languages


Under construction

Last edited Jun 4, 2014 at 5:35 PM by andrewjkennedy, version 5