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.
Tag
Verification
14 notes
Separation Logic for Managed (GC'd) Heaps
Iris-based separation logics with space credits, tracing GC, and the 2025 IrisFit + Nextgen-Modality lines.
Formal Models of the Rust Borrow Checker
Stacked Borrows, the 2025 Tree Borrows replacement, and the trajectory of NLL / two-phase formalisation.
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.
CompCert and the Verified-Compiler Toolchain
The production-grade formally verified C compiler, the CompCertO / Owlang line, and why it matters for JIT verification.
Aeneas
Rust verification by functional translation: compile Rust to a pure lambda calculus, verify there.
Kani
AWS's bit-precise bounded model checker for Rust, deployed in CI on Firecracker and the standard library.
Creusot
A deductive verifier for safe Rust that compiles to Why3 and discharges to off-the-shelf SMT solvers.
Verus
Microsoft Research's SMT-backed Rust verifier, the leading tool for verified systems software at scale in 2025-2026.
RustBelt and Iris
Foundational separation-logic verification of Rust's safe / unsafe core, and its 2024-2026 RefinedRust successor.
Formal Verification and Mechanized Safety
RustBelt/Iris, Verus, Creusot, Kani, Aeneas, CompCert, CakeML, Stacked/Tree Borrows, separation logic for managed heaps, capability-machine logics.
Chapter 20. Logic in Programming
Logic programming, type systems, verification, model checking, and program synthesis.
Chapter 20. Logic in Programming
Logic programming, type systems, verification, model checking, and program synthesis.
9.5 Reproducibility and Verification
How to make computational results repeatable, checkable, and trustworthy.