Verasco is a static analyzer for the CompCert subset of ISO C 1999 that establishes the absence of run-time errors in analyzed programs. The analyzer is based on abstract interpretation and combines several abstract domains, non-relational (integer intervals, floating-point intervals, integer congruences, points-to properties) and relational (integer linear inequalities, symbolic equalities). Verasco enjoys a modular structure roughly inspired by that of Astrée. The major novelty of Verasco, compared with other static analysis tools, is that it is entirely specified and proved sound using the Coq proof assistant. Verasco’s proof guarantees, with mathematical certainty, that programs that analyze without alarms are free of run-time errors.