Verifiable C is a program logic for the C programming language:
foundational higher-order impredicative concurrent separation logic, proved sound with respect to the operational semantics of CompCert C

Books and documentation

Program Logics for Certified Compilers PLCC excerpt to chapter 3 Verifable C
(e-book)  (Kindle)
Free up to Chapter 3 Free download

Software downloads

Verifiable C is a component of the Verified Software Toolchain