Skip to content
Matthieu Sozeau edited this page Mar 12, 2026 · 12 revisions

Welcome to the CertiRocq wiki. The Wiki provides documentation for the CertiRocq compiler.

CERTIROCQ_LOGO-inline-1

Contents

  1. The CertiRocq Plugin
    Useful information about the usage of the CertiRocq plugin.
  2. The bootstrapped CertiRocqC and CertiRocqChk Plugins
    Useful information about the bootstrapped plugins.
  3. The CertiRocq Pipeline
    Information about the CertiRocq pipeline and its current verification status.
  4. Glue Code and FFI
    Information about interfacing with the generated C code.
  5. Memory Model and Garbage Collection
    Lightweight description of CertiRocq's memory representation and runtime.
  6. When C code allocates on the Rocq heap
    How to write C functions that interface with Rocq functions

Clone this wiki locally