Verified Software Toolchain    DOWNLOADS

Verified Software Toolchain (Coq development)

Current release:
VST version 2.2 (June 2018), compatible with CompCert 3.3 (or CompCert 3.2) and Coq 8.8.0 (or Coq 8.7).

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