Formally verified C compiler

Current versions:

stable 3.2
bottle 🍾 high_sierra, sierra, el_capitan


--with-config-x86_64 Build Compcert with ./configure 'x86_64'

Depends on when building from source:

coq 8.8.0 Proof assistant for higher-order logic
menhir 20171222 LR(1) parser generator for the OCaml programming language
ocaml 4.06.1 General purpose programming language in the ML family

JSON API for compcert

Formula code on GitHub

Fork me on GitHub