Rust Formal Methods Interest Group

The RFMIG provides a forum for academics, industry users and any other interested party discuss and collaborate on the challenges of Rust program verification.

Our objectives are to:

Improve communication between formal tool developers and the Rust core teams

• Hold 'office hours' with Rust team members to answer questions about the rustc API or the direction of the language.
• Identify weak points in Rust's current tool interfaces, help shepherd the improvements the formal methods community needs.

Foster a community of formal methods tools and users

• Provide a platform for tool developers to share their work and encourage collaboration.
• Gather feedback and input from industrial and hobbyist users of formal method tooling.
• Work towards improving tool inter-compatibility, in particular of specifications.

Meetings

Upcoming Meetings

• November 25 - Aquascope: Improving Ownership Understanding with Datalog, Compilers, and Diagrams
  Modern programming languages have increased in complexity. Although type systems provide desirable program guarantees, such as Rust’s beloved ownershi…

Past Meetings

• October 28 2024 - Towards Sound `unsafe` Rust
  Rust guarantees memory safety and data race freedom through its type checker, which enforces ownership and borrowing rules. However, adhering strictly…
• September 30 2024 - Contracts in Rust
  As the growing number of verification tools (Aeneas, Creusot, Kani, Prusti, Verus, ...) has shown, there is a growing community for formal verificatio…
• May 27 2024 - Debugging SMT issues: Axiom Profiler 2.0
  The majority of automated verification tools rely on SMT solvers for logical reasoning. Often tools spend most of the verification time querying them.…
• May 25 2024 - Gillian-Rust: A hybrid approach to unsafe Rust verification
  The Rust Formal Methods Interest group has seen several talks about scalable verification of safe Rust (Prusti, Creusot, Aeneas, Flux…), and other ana…
• January 22 2024 - Modernizing verified crypto with Rust: introducing HACL-Rust and Eurydice
  The program verification community is slowly realizing that life is much better when one verifies Rust programs instead of C or ASM programs. Yet, a l…
• November 27 2023 - Verifying a Concurrent Memory Allocator with Verus
  2023-11-27 mimalloc verus I will present ongoing work in verifying a concurrent memory allocator using Verus [1], a deductive verification tool for Ru…
• September 25 2023 - Type Invariants in Creusot
  Type invariants are a common mechanism in program verification, that allows attaching logical predicates to data types. They typically capture propert…
• May 29 2023 - Tree Borrows, a pointer aliasing model for Rust
  The strong guarantees of unique ownership and immutability provided by reference types in Rust should in principle allow compilers to apply more power…
• March 27 2023 - Flux: Ergonomic Verification of Rust Programs with Liquid Types
  Low-level, pointer-manipulating programs are tricky to write and devilishly hard to verify, requiring complex spatial program logics to reason about h…
• January 30 2023 - Leveraging Rust Types for Program Synthesis
  This talk will explore how one can apply ideas from verification to synthesize Rust function bodies given a signature and possibly some functional ann…
• November 28 2022 - MiniRust with Ralf Jung
  As Rust grows in popularity and usage, it is becoming more and more important to clearly define its operational semantics. Despite plenty of work on R…
• October 24 2022 - Aeneas
  We present Aeneas, a new verification toolchain for Rust programs based on a lightweight functional translation. We leverage Rust's rich region-based …
• September 26 2022 - CreuSAT
  This talk describes CreuSAT, a formally verified SAT solver written in Rust. In addition to implementing the core conflict-driven clause learning (CDC…
• May 30 2022 - CRUX MIR
  crux-mir is a symbolic testing tool for Rust. The user writes test cases using symbolic variables as inputs; crux-mir uses symbolic execution to chec…
• April 25 2022 - Ferrocene
  Ferrocene is an effort to bring Rust into the realm of safety-critical software while also bringing tangible benefits to so called mission-critical ef…
• March 28 2022 - Kani
  Kani is a Rust verification tool based on model checking. With Kani, you can ensure that broad classes of problems are absent from your Rust code by w…
• February 28 2022 - Creusot
  Xavier Denis will discuss Creusot, his deductive verifier for Rust. Creusot aims to provide efficient verification of complex safe Rust code, and is b…
• January 31 2022 - MIRAI
  Herman Venter gave a retrospective view of his work on MIRAI, an abstract interpreter for MIR code. We went over key design choices for abstract inter…
• November 29 2021 - CONCERT and HACSPEC
  Rust is a big and complex language. Fortunately, it contains a number of interesting sublanguages for which formal verification is more manageable. I …
• October 25 2021 - Verification Challenge
  Unfortunately this meeting was not record (my bad). We discussed the specifications for a few simple functions in Prusti and Creusot. There were quit…
• September 21 2021 - Inaugural Meeting
  During this meeting, we will introduced the RFMIG, and had a presentation from Vytautas Astraukas of Prusti, showing a little glimpse of verification …

Interesting projects

These initiatives may interest the developers of formal methods tools for Rust, don't hesitate to join the discussion on Zulip.

• Project Stable MIR: An effort to define a semi-stable API boundary for the Rust compiler specifically targeting verification usecases.
• Project Ghost Code: An experiment to define a generic notion of 'ghost code' for use in the compiler which would enable verification tools to more easily encode their invariants.