![Iapyx removing arrowhead from Aeneas Iapyx removing arrowhead from Aeneas](https://github.com/AeneasVerif/aeneas/raw/main/static/Aeneas.jpg)
Aeneas (pronunced [Ay-nay-as]) is a verification toolchain for Rust programs. It relies on a translation from Rusts's MIR internal language to a pure lamdba 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.
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).
You need to install OCaml, together with some packages.
We suggest you to follow those instructions, and install OPAM on the way (same instructions).
Any recent version of OCaml 4 should do. For instance, if you want to use OCaml 4.14.2:
opam switch create 4.14.2
You can then install the dependencies with the following command:
opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc \
unionFind ocamlgraph menhir ocamlformat
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.
If you run make
, you will generate a documentation accessible from doc.html
.
The Aeneas binary is in bin
; you can run: ./bin/aeneas -backend {fstar|coq|lean|hol4} [OPTIONS] LLBC_FILE
,
where LLBC_FILE
is an .llbc file generated by Charon.
Aeneas provides a lot of flags and options to tweak its behaviour: you can use --help
to display a detailed documentation.
Files generated by the Lean backend import the Base
package from Aeneas.
To use those files in Lean, create a new Lean package using lake new
,
overwrite the lean-toolchain
with the one inside ./backends/lean
,
and add base
as a dependency in the lakefile.lean
:
require base from "PATH_TO_AENEAS_REPO/backends/lean"
We target safe Rust. This means we have no support for unsafe Rust, though we plan to design a mechanism to allow using Aeneas in combination with tools targeting unsafe Rust.
We have the following limitations, that we plan to address one by one:
- loops: no nested loops for now. We are working on lifting this limitation.
- no functions pointers/closures: ongoing work. We have support for traits and will have support for function pointers and closures soon.
- limited type parametricity: it is not possible for now to instantiate a type parameter with a type containing a borrow. This is mostly an engineering issue.
- no nested borrows in function signatures: ongoing work.
- interior mutability: ongoing work. We are thinking of modeling the effects of interior mutability by using ghost states.
- no concurrent execution: long-term effort. We plan to address coarse-grained parallelism as a long-term goal.
We currently support F*, Coq, HOL4 and Lean. We would be interested in having an Isabelle
backend. Our most mature backends are Lean and HOL4, for which we have in particular
support for partial functions and extrinsic proofs of termination (see
./backends/lean/Base/Diverge/Elab.lean
and ./backends/hol4/divDefLib.sig
for instance)
and tactics specialized for monadic programs (see
./backends/lean/Base/Progress/Progress.lean
and ./backends/hol4/primitivesLib.sml
).
A (basic) tutorial for the Lean backend is available here.
Assuming Nix is installed, with a support for Flakes (*
):
$ # Run Charon with the exact same version required by Aeneas
$ nix run github:aeneasverif/aeneas#charon -L
$ nix run github:aeneasverif/aeneas -L -- -backend your_preferred_backend your_llbc.file
To regenerate the extraction, just run step 2 and step 3 again.
(*)
: Flakes are not necessary, here is an example of how to do similar steps without it:
$ nix-shell '<aeneas>' -A packages.x86_64-linux.charon --run "charon" -I aeneas=https://github.com/AeneasVerif/aeneas/archive/main.tar.gz
$ nix-shell '<aeneas>' -A packages.x86_64-linux.default --run "aeneas --backend your_preferred_backend your_llbc.file" -I aeneas=https://github.com/AeneasVerif/aeneas/archive/main.tar.gz
The translation has been formalized and published at ICFP2022: Aeneas: Rust verification by functional translation (long version). We also have a proof that the symbolic execution performed by Aeneas during its translation correctly implements a borrow checker, and published it in a preprint.