An introduction to proving theorems and certifying programs with Coq. The accompanying slides can be found here.
Make sure you have the dependencies listed below. Then you can run make to verify the proofs. The build artifacts can be removed with make clean.
The build system depends on the following:
You also need the usual set of Unix tools, such as echo, find, etc.