The general aim of this project is to use the idea of developing program verification tools with proofs of soundness in Coq to make Foundational Proof-Carrying Code practical enough to use at all levels of computer systems.
To download the source distribution, follow the instructions in the documentation for checking out the CVS repository.
Author: Adam Chlipala