Formally verified C compiler

Current version

compcert requires the following formulae to be installed:
coq 8.7.2 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

Recent formula history

ilovezfs compcert 3.2
ilovezfs compcert: depend on ocaml-num
ilovezfs compcert: build with Coq 8.6.1 from OPAM (#19742)
ilovezfs Use “squiggly” heredocs.
Benjamin Beurdouche compcert 3.1

Formula code at GitHub