Welcome to x86proved

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

Requirements

To use x86proved you will need You can obtain all three bundled for 32-bit and 64-bit Windows from Pierre-Yves Strub's web page.
You will need either

Install

Under construction

Contribute

There are many ways to contribute to x86proved.

Documentation

Under construction