| layout |
|---|
home |
The AeneasVerif organization is an umbrella for several Rust verification projects. Its flagship project is Aeneas (pronunced [Ay-nay-as]), a toolchain to translate safe Rust programs to functional models in a variety of proof assistants, including F*, Coq, HOL4 and Lean.
Read more about our work on the [Projects]({% link projects.markdown %}) page, or join us on Zulip!