Verified Software Toolchain    DOWNLOADS

Verified Software Toolchain (Coq development)

Current release:
VST version 2.0 (January 2018), compatible with CompCert 3.2 and Coq 8.7.1.

Bleeding edge: VST Git repository

Previous releases: here

Documentation:

Verifiable C: Applying the Verified Software Toolchain to C programs (also included in doc/ directory of VST distribution).

Program Logics for Certified Compilers, by Andrew W. Appel et al., Cambridge University Press, 2014.
E-book; Hardback from publisher; Hardback from Amazon.com