The Coq mailing list

[Andrew Appel <appel AT CS.Princeton.EDU>]

I am pleased to announce release 2.0 of the Verified Software Toolchain.

This release includes the Verifiable C program logic, compatible with
the recently released CompCert 3.2 and Coq 8.7.1.

Verifiable C is a program logic based on higher-order separation logic
for the C programming language.  Users work interactively in Coq
to verify their C programs (as parsed by the front end of CompCert),
applying "symbolic execution" proof-automation tactics.  VST is
proved sound with respect to the operational semantics of CompCert
Clight -- so if you compile the rest of the way with CompCert you
get a machine-checked guarantee that the assembly language program
conforms to the functional specification you proved.  But you can
also compile with gcc or clang, and it's compatible (though not provably).

Since the last major release, there have been many improvements in usability
and in proof automation.  The user manual has been rewritten and improved.

VST has been used to verify the following C programs:

SHA-256 cryptographic hashing (from openSSL)
HMAC cryptographic authentication (from openSSL)
HMAC-DRBG crypto random number generation (from mbedTLS)
Other crypto primitives: HKDF, tweetnacl, AES encryption
Sensor/controller concurrent messaging system (installed in an autonomous heavy truck)
Small example programs included with distribution: linked lists, queues, binary search trees, arrays, etc.

Several other C-program verifications are underway in California, Pennsylvania, Singapore, Netherlands, and New Jersey.