AeneasVerif / aeneas

Unknown author, Iapyx removing arrowhead from Aeneas [Fresco].
Wall in Pompei, digital image from Michael Lahanis.
 Source 
# Aeneas
Aeneas (pronunced [Eh-nee-as]) is a verification toolchain for Rust programs. It relies on a translation from Rust's MIR
internal language to a pure lambda calculus. It is intended to be used in combination with
Charon, which compiles Rust programs to an intermediate
representation called LLBC. It currently has backends for F\*,
Coq, HOL4 and LEAN.
If you want to contribute or ask questions, we strongly encourage you to join the
Zulip. In particular, we welcome external
contributions but ask contributors to engage with us before making deep modifications of
the code or implementing non trivial features, as these require in-depth design
discussions and careful reviews. If you want to contribute a new feature you should either
discuss it on the Zulip or open the corresponding issue on github.
## Project Structure
- `src`: the OCaml sources. Note that we rely on Dune
 to build the project.
- `backends`: standard libraries for the existing backends (definitions for
 arithmetic operations, for standard collections like vectors, theorems, tactics, etc.)
- `tests`: files generated by applying Aeneas on some of the test files of Charon,
 completed with hand-written files (proof scripts, mostly).
## Installation & Build
You need to install OCaml, together with some packages.
We suggest you to follow those instructions,
and install OPAM on the way (same instructions).
We are developing Aeneas by using **OCaml 5**. For instance, if you want to use OCaml 5.3.0:
 [code] 
You can then install the dependencies with the following command:
 [code] 
Moreover, Aeneas uses the Charon project and library.
For Aeneas to work, `./charon` 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`
(this uses either rustup or nix to build Charon, depending on which one is installed).
In case of version mismatch, you will be instructed to update Charon.
If you're also developing on Charon, you can instead set up `./charon` to be a symlink to your local version:
`ln -s PATH_TO_CHARON_REPO charon`. In this case, the scripts will not check that your Charon
installation is on a compatible commit. When you pull a new version of Aeneas, you will occasionally
need to update your Charon repository so that Aeneas builds and runs correctly.
Finally, building the project simply requires running `make` in the top
directory.
You can also use `make test` and `make verify` to run the tests, and check
the generated files. As `make test` will run tests which use the Charon tests,
you will need to regenerate the `.llbc` files. To do this, run `make setup-charon` before `make
test`. Alternatively, call `REGEN_LLBC=1 make test-...` to regenerate only the needed files.
## Documentation
If you run `make`, you will generate a documentation accessible from `doc.html`.
Additi