# Aeneas turns Rust MIR into a pure lambda calculus for proof assistants

> Aeneas is an OCaml verification toolchain that translates Rust's MIR into a pure lambda calculus, then emits proofs for F*, Coq, HOL4 or Lean. It is built for Rust developers who need machine checked proofs, and it currently covers a subset of safe Rust only.

**AeneasVerif/aeneas** — A verification toolchain for Rust programs

- Repository: https://github.com/AeneasVerif/aeneas
- Website: https://aeneasverif.github.io/
- Stars: 1,095 · Forks: 133
- Language: OCaml
- License: Apache-2.0
- Published: 2026-10-19 · Updated: 2026-10-19 · Language: en
- Canonical page: https://hysenlabs.com/projects/aeneasverif-aeneas

## Aeneas translates MIR, so the Rust you verify must be compilable Rust

Aeneas is a verification toolchain for Rust programs, and it is not a Rust linter or a fuzzing harness. The README describes it as a toolchain that relies on a translation from Rust's MIR internal language to a pure lambda calculus. MIR is the mid-level IR that rustc produces after type checking and borrow checking, so by the time Aeneas sees a program, the ownership discipline has already been enforced by the compiler.

That placement in the pipeline explains both the value and the limits of the project. Programs that type check and borrow check can be handed to a theorem prover, where a human or a solver can reason about behaviour that the compiler cannot check. A pure lambda calculus is the right target for that job, since it is a small, well understood language that every major prover can represent.

The audience is narrow and technical. The README positions Aeneas for use together with Charon, the Rust to LLBC compiler, and lists backends for F*, Coq, HOL4 and Lean. The topics attached to the project include formal verification, deductive reasoning, Coq, F*, HOL4 and Lean, which is an accurate picture of the ecosystem it plugs into. If you want a tool that verifies a running system end to end, this is not it. If you want a proof artifact for a specific algorithm or data structure in safe Rust, it is aimed squarely at that.

## The charon-pin file is the contract between Aeneas and Charon

Aeneas does not parse Rust itself. Charon compiles Rust programs into an intermediate representation called LLBC, and Aeneas consumes that. The hand-off is pinned rather than floating: for Aeneas to work, the ./charon directory must contain a clone of the Charon repository at the commit specified in ./charon-pin. The easiest way to set this up is to call make setup-charon, which uses either rustup or nix to build Charon, depending on which one is installed. If the versions do not match, you are instructed to update Charon.

Developers who also work on Charon can point ./charon at a symlink to their own checkout instead. The trade-off is spelled out in the documentation: when you use a symlink, the scripts do not check that your Charon installation is on a compatible commit. In exchange for that skipped check, you will occasionally need to update your Charon repository after pulling a new version of Aeneas, so that Aeneas builds and runs correctly.

This pin is the single most important operational detail for anyone running the toolchain in CI. A build that breaks after an Aeneas update is usually a Charon commit that has moved, not a broken toolchain. The repository layout backs this up: src holds the OCaml sources, backends holds the standard libraries for each backend with definitions for arithmetic operations, standard collections such as vectors, theorems and tactics, and tests holds files generated by applying Aeneas to some of the Charon test files, completed with hand written proof scripts.

## Building Aeneas means an OCaml 5 switch, opam, Dune and a pinned Charon

Installation is a source build, and the documentation asks you to install OCaml along with some packages, following the OCaml installation instructions and installing OPAM on the way. The project is developed using OCaml 5, and the README shows a switch creation command for a specific compiler version:

```bash
opam switch create 5.3.0
```

With the switch in place, the dependencies are installed with:

```bash
opam install src --deps-only --with-test
```

After that comes the Charon clone described above, either through make setup-charon or through a symlink. The final build step is deliberately short, since Dune handles the OCaml side:

```bash
make
```

The Makefile adds a few details worth knowing. The default target builds, while all runs build-tests-verify plus nix. Paths to the executables are overridable variables: AENEAS_EXE points at $(PWD)/bin/aeneas, the test runner at $(PWD)/bin/test_runner, and CHARON_EXE at $(PWD)/charon/bin/charon. The Rust toolchain commands default to rustc +nightly and cargo +nightly, which is why the Makefile comments suggest overriding them with plain rustc and cargo inside Nix, where the toolchain is already nightly. The build rule itself runs dune build inside src, and a second target builds the OCaml library aeneas.cmxs for use as a plugin.

There is a guard rail worth noting. The Makefile refuses to run on make 3.81, the version shipped with macOS, and prints a hint to install make and invoke gmake. Formatting is enforced in CI, while a local build skips that step, and IN_CI also activates the expensive sanity checks.

## Generating an llbc file with the aeneas preset, then running the backend

The first real use has two halves. First you generate the serialized .llbc file by calling Charon from inside, similarly to cargo, the crate you want to translate. The documentation marks the preset option as important, so the call is:

```bash
charon cargo --preset=aeneas
```

Second, you run the Aeneas binary, which lives in the bin directory, on the .llbc file Charon produced:

```bash
./bin/aeneas -backend {fstar|coq|lean|hol4} [OPTIONS] LLBC_FILE
```

Here LLBC_FILE is an .llbc file generated by Charon. The four backend names are listed exactly as shown, and the tool exposes a lot of flags and options to tweak its behaviour, with --help printing a detailed documentation.

Tests and generated files can be checked with make test and make verify. Because the test suite uses the Charon tests, the .llbc files have to be regenerated first, which means running make setup-charon before make test. If you only want to refresh the files you actually changed, there is a narrower escape hatch:

```bash
REGEN_LLBC=1 make test-...
```

Running make also generates documentation, reachable at doc.html in the top level directory. A tutorial for the Lean backend ships in the repository under tests/lean/Tutorial, with the original Rust file at tests/src/tutorial/src/lib.rs, and it requires a working installation of Lean.

## The Lean backend needs a lake package pointing at backends/lean

Using the Lean backend takes extra steps that the other backends do not need. Files generated by the Lean backend import the Aeneas package from Aeneas itself, so the consuming project has to declare that dependency.

The documented sequence is: create a new Lean package using lake new, overwrite the lean-toolchain with the one inside ./backends/lean, and then add aeneas as a dependency in the lakefile.lean:

```lean
require aeneas from "PATH_TO_AENEAS_REPO/backends/lean"
```

The same dependency can be expressed in the lakefile.toml instead:

```toml
[[require]]
name = "aeneas"
path = "PATH_TO_AENEAS_REPO/backends/lean"
```

If you do not have Aeneas cloned locally, the documentation says you can specify the dependency using the GitHub repository, and suggests adding a specific commit hash so that future updates do not break your project:

```toml
[[require]]
name = "aeneas"
git = { url = "https://github.com/AeneasVerif/aeneas", subDir = "backends/lean" }
rev = "COMMIT_HASH_HERE"
```

The commit hash advice is the practical takeaway here. A Lean project that tracks a moving branch of the backend standard library can break when the library changes, and the fix is to pin a revision. The repository also ships a flake.nix, a shell.nix and a default.nix, so a Nix based environment is a supported route for pinning the toolchain as well.

## Break to an outer loop and generic mutable references are still rejected

Aeneas currently functionalizes a subset of safe Rust, and the documentation is unusually honest about where that subset ends. The stated limitations on the safe subset are described as technical rather than fundamental, with plans to address them one by one depending on user needs.

The first limitation concerns control flow. A return inside nested loops, or a break or continue targeting an outer loop, is not supported yet, with the example given being a labelled break out of a double loop. The second concerns types. Instantiating a generic type, including Self through a trait implementation, with a mutable reference is not supported, with the example given being a call to id(&mut x) where the function is fn id<T>(x: T) -> T.

Two larger gaps are on the roadmap rather than the current menu. Unsafe code and concurrency are both listed as limitations that will be lifted by the ongoing work on separation logic, and the project describes extending the functional model with reasoning based on separation logic to support unsafe code and concurrent code. The separation logic work is therefore not a detail, it is the stated path to covering the parts of Rust that the type system alone cannot vouch for.

The practical consequence for an engineer is that you cannot assume arbitrary safe Rust will translate. A proof effort will stall on constructs that look entirely ordinary, and the workaround is usually to restructure the code so the unsupported pattern disappears.

## Lean and HOL4 are the most mature backends, and releases ship nightly

The backend list covers F*, Coq, HOL4 and Lean, and the README states that the most mature backends are Lean and HOL4. The project would be interested in having an Isabelle backend, which tells you something about where the effort has gone and where the gaps are. When a backend is immature, the practical symptom is usually the standard library under backends, where the definitions for arithmetic operations, standard collections like vectors, theorems and tactics live per backend.

Release cadence follows the proof assistant world rather than the software world. The recent tags are nightlies named for their date and commit, for example nightly-2026.10.15-cd41995 on 2026-10-15, nightly-2026.10.14-bbc0151 on 2026-10-14 and nightly-2026.10.13-73b7cf9 on 2026-10-13. The repository is not archived, and the last push was on 2026-10-19. There is no sign of a stable release train in that list, so anyone planning a deployment should expect to track a specific commit rather than wait for a version number.

The licence is Apache-2.0, which is permissive for a toolchain and does not impose the copyleft obligations that a GPL component would. That is a licensing statement rather than legal advice, and the LICENSE.md file in the repository is the authoritative text. The contribution process has its own friction: the README asks contributors to join the Zulip and engage before making deep modifications of the code or implementing non trivial features, because those need in-depth design discussions and careful reviews. A new feature should be discussed on the Zulip or raised as an issue first.

## Conclusion

Adopt Aeneas if you are writing safe Rust that needs a machine checked proof in Lean, HOL4, F* or Coq, and you are prepared to live inside the supported subset, which currently excludes break and continue targeting an outer loop and generic instantiation with a mutable reference. Do not expect it to handle unsafe code or concurrency yet, since both wait on the separation logic work. Before you start, check that charon-pin matches the Charon commit you clone, decide whether the Lean backend is worth the lake package setup, and confirm that your Rust crates can be compiled by Charon with the aeneas preset.

## FAQ

### What does Aeneas actually do with a Rust program?

It translates the program's MIR internal language into a pure lambda calculus. Aeneas does not parse Rust directly, it consumes the LLBC intermediate representation produced by Charon.

### How do I install Aeneas and get Charon in place?

Install OCaml and OPAM, create a switch such as opam switch create 5.3.0, run opam install src --deps-only --with-test, then run make setup-charon to clone and build Charon at the commit in charon-pin. Finally run make in the top directory, and the binary appears in bin.

### Can Aeneas verify unsafe Rust or concurrent Rust today?

No. Aeneas currently functionalizes a subset of safe Rust, and the documentation lists unsafe code and concurrency among the limitations that will be lifted by the ongoing work on separation logic.

### Why does my Lean project fail to compile the files Aeneas generates?

Files generated by the Lean backend import the Aeneas package from Aeneas, so the project must require aeneas from the backends/lean directory, overwrite its lean-toolchain with the one in that directory, and pin a commit hash if it references the GitHub repository.

### Which proof backends does Aeneas support?

The current backends are F*, Coq, HOL4 and Lean, and the documentation names Lean and HOL4 as the most mature. The project states it would be interested in adding an Isabelle backend.

## Sources

- [AeneasVerif/aeneas on GitHub](https://github.com/AeneasVerif/aeneas)
- [License: Apache-2.0](https://github.com/AeneasVerif/aeneas/blob/main/LICENSE)
- [Project website](https://aeneasverif.github.io/)
- [README](https://github.com/AeneasVerif/aeneas/blob/main/README.md)
- [Releases](https://github.com/AeneasVerif/aeneas/releases)

---

Hysen Labs editorial analysis, written from the project's own repository and release notes. Cite the canonical page: https://hysenlabs.com/projects/aeneasverif-aeneas