Verified Software Toolchain    DOWNLOADS

Verified Software Toolchain (Coq development)

Current release:
VST version 2.4 (April 2019), compatible with CompCert 3.5 (or CompCert 3.4) and Coq 8.9.0.

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