# Chamois CompCert Chamois CompCert is a fork of CompCert, the formally verified C compiler. For an up-to-date presentation, see [our OOPSLA'23 paper](https://hal.science/hal-04102940). ## Overview The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM, x86 and RISC-V processors. The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code. For more information on CompCert (authors, supported platforms, supported C features, installation instructions, using the compiler, etc), please refer to the [Web site](https://compcert.org/) and especially the [user's manual](https://compcert.org/man/). ## Chamois version Chamois CompCert is a version of CompCert with additions from [Verimag](https://www-verimag.imag.fr) and previously from [Kalray](https://www.kalrayinc.com/) (a chamois is a fast and agile caprine, very common in French Alps).