The Peregrine Project provides a unified middle-end for code generation from proof assistants. It supports Agda, Lean, and Rocq and can generate code in CakeML, C, Rust, OCaml.
It puts a focus on correct code extraction: The middle end is verified in the Rocq proof assistant, and some of the frontends and backends are. It is based on an intermediate language called lambda box.
Frontends:
Backends:
- CakeML
- C using CertiCoq and then x86,ARM, RISCV using CompCert.
- Rust using ConCert
- OCaml, verified
- Wasm, verified using CertiRocq-wasm
Team Members: James Chapman, Simon Dima, Lucas Escot, Yannick Forster, Orestis Melkonian, Eske Nielsen, Matthieu Sozeau, Bas Spitters.
Contributors: Hugo Segoufin-Chollet.
Supported by: INRIA, Aarhus University, IOG, Ethereum.