DeepSpec
 
The Science of Deep Specification
Verified Software Toolchain
VST diagram

The Verified Software Toolchain is a toolchain for verifying C code inside the Coq proof assistant, in a higher-order concurrent, impredicative separation logic ("Verifiable C") that is provably sound w.r.t.~the Clight operational semantics of CompCert. Current work is focused on enhancing automation support ("Floyd"), particularly for well-synchronized concurrent programs executing on processors with weakly cache-coherent memory models, formally connecting the VST to other DeepSpec components (CertiKOS, CertiCoq, Vellum), and verifying high-assurance application components, including mailbox-style message delivery systems and cryptographic libraries.

Verified Software Toolchain project website