VST

Verified Software Toolchain

From PrincetonUniversity·Updated June 16, 2026·View on GitHub·

[Andrew W. Appel](http://www.cs.princeton.edu/~appel/), [Lennart Beringer](http://www.cs.princeton.edu/~eberinge/), [Robert Dockins](http://rwd.rdockins.name/), [Josiah Dodds](http://www.cs.princeton.edu/~jdodds/), [Aquinas Hobor](http://www.comp.nus.edu.sg/~hobor/), [Jean-Marie Madiot](https://madiot.fr/), [Gordon Stewart](http://www.cs.princeton.edu/~jsseven/), [Qinxiang Cao](http://jhc.sjtu.edu.cn/people/members/faculty/qinxiang-cao.html), Qinshi Wang, and others. The project is written primarily in Rocq Prover, distributed under the Other license, first published in 2014. Key topics include: c, compcert, coq, coq-library, coq-vst.

Latest release: v3.1beta2— VST version 3.1beta2

June 16, 2025View Changelog →

Verified Software Toolchain

with contributions from

Andrew W. Appel,
Lennart Beringer,
Robert Dockins,
Josiah Dodds,
Aquinas Hobor,
Jean-Marie Madiot,
Gordon Stewart,
Qinxiang Cao,
Qinshi Wang,
and others.

The LICENSE file has information about copyright, licensing, and permissions.

How to install:

See here for instructions.

Documentation:

Our webpage describes the goals of the project
and has links to many related publications.

For an introduction to how to use Verifiable C,
read the manual,
or consult Software Foundations Volume 5: Verifiable C
for a tutorial with exercises.

Program Logics for Certified Compilers, by Andrew W. Appel et al.,
Cambridge University Press, 2014.
Available in hardcover.