Verified Software Toolchain    DOWNLOADS

Verified Software Toolchain (Coq development)

Current release:
VST version 2.3 (January 2019), compatible with CompCert 3.4 (or CompCert 3.3) and Coq 8.8.0 (or Coq 8.8.2).

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