HOW TO INSTALL

Releases 2.7, 2.8, 2.9, and later are distributed through the Coq Platform and listed at the VST github. Releases 2.6 and earlier are available at this archive.

Documentation:

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

Software Foundations Volume 5: Verifiable C, by Andrew W. Appel and Qinxiang Cao, 2020.

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

Note about CompCert noncommercial license

VST relies on CompCert for some purposes. The CompCert license permits some parts of CompCert to all users, and other parts only to licensed users. Whether or not you are a licensed user, you may use VST; but only licensed users may process .c files through CompCert's clightgen tool (among other things).

You are a licensed user if your use "relates only to educational, research, personal or evaluation purposes" or if you have purchased a license from AbsInt.com.

If you are licensed user, you may use full CompCert, by doing
opam install coq-compcert.3.7+8.12~coq_platform

If you are not a licensed user, you may use only the open-source portions of CompCert. Before installing coq-vst, install CompCert by:
opam install coq-compcert.3.7+8.12~coq_platform~open_source