Rust Formal Methods IG
The Rust Formal Methods IG is a community group interested in the design and development of formal methods tooling for the Rust programming language
Place Capability Graphs
Taming Unsafe Code with Safety Tags
RefinedRust
AquaScope
VTock: Verifying the Tock Kernel
Towards Sound `unsafe` Rust
Contracts, Revisited
Gillian Rust: A hybrid approach to unsafe Rust verification
Modernizing verified crypto with Rust: introducing HACL-Rust and Eurydice
Verifying a Concurrent Memory Allocator with Verus
Type invariants in Creusot
Tree Borrows: An aliasing model for Rust
Flux: Ergonomic Verification of Rust Programs with Liquid Types
Verus -- SMT-based verification of Rust systems code
Leveraging Rust Types for Program Synthesis
MiniRust: An operational semantics for Rust
Aeneas: Aeneas Verification by Functional Translation
RFMIG: CreuSAT, a verified SAT solver
Flowistry -- Modular information flow analysis for Rust
May Session -- CRUX MIR
March Session -- Kani
February Session -- Creusot
January Session -- MIRAI
November Meeting -- Bas Spitters
Inaugural Meeting -- 20/09/2021