Formal Verification and Mechanized Safety

RustBelt/Iris, Verus, Creusot, Kani, Aeneas, CompCert, CakeML, Stacked/Tree Borrows, separation logic for managed heaps, capability-machine logics.

10 items

Research › Memory Management › Formal Verification and Mechanized Safety ›

RustBelt and Iris

Foundational separation-logic verification of Rust's safe / unsafe core, and its 2024-2026 RefinedRust successor.
memory-safety verification May 18, 2026
Research › Memory Management › Formal Verification and Mechanized Safety ›

Verus

Microsoft Research's SMT-backed Rust verifier, the leading tool for verified systems software at scale in 2025-2026.
memory-safety verification May 18, 2026
Research › Memory Management › Formal Verification and Mechanized Safety ›

Creusot

A deductive verifier for safe Rust that compiles to Why3 and discharges to off-the-shelf SMT solvers.
memory-safety verification May 18, 2026
Research › Memory Management › Formal Verification and Mechanized Safety ›

Kani

AWS's bit-precise bounded model checker for Rust, deployed in CI on Firecracker and the standard library.
memory-safety verification May 18, 2026
Research › Memory Management › Formal Verification and Mechanized Safety ›

Aeneas

Rust verification by functional translation: compile Rust to a pure lambda calculus, verify there.
memory-safety verification May 18, 2026
Research › Memory Management › Formal Verification and Mechanized Safety ›

CompCert and the Verified-Compiler Toolchain

The production-grade formally verified C compiler, the CompCertO / Owlang line, and why it matters for JIT verification.
memory-safety verification May 18, 2026
Research › Memory Management › Formal Verification and Mechanized Safety ›

CakeML and the Verified-JIT Line

The bootstrapping verified ML compiler, its 2024 PLDI agenda, and the FM-JIT verified-JIT effort that builds on it.
memory-safety verification May 18, 2026
Research › Memory Management › Formal Verification and Mechanized Safety ›

Formal Models of the Rust Borrow Checker

Stacked Borrows, the 2025 Tree Borrows replacement, and the trajectory of NLL / two-phase formalisation.
memory-safety verification May 18, 2026
Research › Memory Management › Formal Verification and Mechanized Safety ›

Separation Logic for Managed (GC'd) Heaps

Iris-based separation logics with space credits, tracing GC, and the 2025 IrisFit + Nextgen-Modality lines.
memory-safety verification May 18, 2026
Research › Memory Management › Formal Verification and Mechanized Safety ›

Capability-Machine Formalism and Endorsement Relations

Cerise, the CHERI-C Coq memory model, and capability-safety logical relations as the formal model behind handle-based runtimes.
memory-safety verification May 18, 2026