Aeneas: Rust Verification by Functional Translation

Add to your list(s) Download to your calendar using vCal

• Son Ho (Azure Research team)
• Friday 30 May 2025, 14:00-15:00
• SS03, Computer Laboratory.

If you have a question about this talk, please contact Ioannis Markakis.

We present Aeneas, a verification toolchain for Rust programs based on a lightweight functional translation. We leverage Rust’s rich region-based type system to generate pure models for a large class of safe Rust programs which can contain shared and mutable borrows, functions returning borrows, traits and loops. Doing so, we allow the user to reason about the original Rust program through the theorem prover of their choice, and enable lightweight verification by eliminating memory reasoning, allowing them to instead focus on functional properties of their code. As of today, Aeneas has backends for F\*, Coq, HOL4 and most importantly Lean, for which we are investing efforts to develop custom tactics and automation. Aeneas is currently being used to verify optimised, low-level cryptographic code, that we will present as well.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• SS03, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list
• yk449

Note that ex-directory lists are not shown.