← All repos

aeneas

A verification toolchain for Rust programs

GitHubaeneasverif.github.io/
compilercoqdeductive-reasoningformal-methodsformal-verificationfstarhol4leanocamlprogram-verificationproofsrustrust-lang
Browse cluster: Lean4 Formal Verification & Cryptography →
5,456commits
46contributors
11languages

Tech stack & purpose

Aeneas is a verification toolchain for Rust programs that translates code to pure functional programs (primarily Lean, but also F*, Coq, and HOL4) for formal verification. The toolchain works by taking Rust's MIR internal language and converting it to a pure lambda calculus, typically in combination with the Charon project which produces an intermediate representation called LLBC. Built in OCaml with the Dune build system, Aeneas currently supports safe Rust with limitations on nested loops, function pointers, closures, and concurrent execution, though the project is actively extending its functional model and has published formalizations of its translation at ICFP 2022 and 2024.

Community & reference links

Languages

OCaml
41.3%
Lean
34.9%
Standard ML
13.3%
Rocq Prover
3.8%
Rust
2.9%
F*
2.9%
Shell
0.3%
Makefile
0.3%
Nix
0.2%
Python
0.0%
Dune
0.0%

Contributors (top 30 of 46)