- Author
- Not stated; the AeneasVerif GitHub organization
- Published
- Undated
- Kind
- Open-source project README
- Original
- github.com/AeneasVerif/aeneas
- Subject
- Formal methods and proof
What it is
The README is published by the AeneasVerif GitHub organization, with no named authors. It explains what the tool does and how to build and run it. It also invites outside contributors through a chat forum.
What it says
- Aeneas translates Rust's MIR into a pure lambda calculus, and works with the tool Charon.
- It has backends for F*, Coq, HOL4 and Lean.
- The README calls Lean and HOL4 the most mature backends.
- Aeneas handles a subset of safe Rust, with gaps in loops and references.
- Unsafe code and concurrency are to be supported later through work on separation logic.
- Missing standard library definitions need hand-written models, which the tool can templatise.
- The README cites an ICFP 2022 paper formalising the translation.
What evidence it gives
The README gives commands, a project layout and a list of limitations. It points to a tutorial, generated tests and two papers. It does not include benchmarks or case studies.
Interests and limits
The authors describe their own project. The README was read in full, but the linked papers, tutorial and tests were not. It admits unsupported features. How far the tool scales on real programs is not shown here.