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.

During the first year of DeepSpec, we

(1) worked towards proving soundness VST's concurrent separation logic w.r.t. relaxed memory models,

(2) developed a new understanding of the semantic models underlying "classical" (or "malloc-free") and "intuitionistic" (or "garbage-collected") separation logic,

(3) verified a new resilient mailbox protocol with low-level concurrency primitives.

(4) The verification of cryptographic primitives led to additional improvements to VST's Floyd automation library.