#verification

Kani

§1 Provenance Project: https://github.com/model-checking/kani ; documentation https://model-checking.github.io/kani/getting-started.html Owned by AWS, open source under MIT/Apache-2.0. Built on the CBMC backend (CPROVER). Production-use case study: AWS Open Source Blog, "Using Kani to Validate Security Boundaries in AWS Firecracker" , 2023, https://model-checking.github.io/kani-verifier-blog/2023/08/31/using-kani-to-validate-security-boundaries-in-aws-firecracker.html Rust standard-library verification initiative (AWS-sponsored, hosted by the Rust Foundation): https://aws.amazon.com/blogs/opensource/verify-the-safety-of-the-rust-standard-library/ ESBMC integration via Goto-Transcoder (Rust Foundation announcement, 2024-2025): https://rustfoundation.org/media/expanding-the-rust-formal-verification-ecosystem-welcoming-esbmc/ Releases through 2025-2026 (Kani 0.61 through 0.66) tracked at https://github.com/model-checking/kani/releases §2...

Creusot

§1 Provenance Denis, Jourdan, Marché. "Creusot: A Foundry for the Deductive Verification of Rust Programs" , FM 2022. https://dl.acm.org/doi/10.1007/978-3-031-17244-1_6 ; preprint https://inria.hal.science/hal-03526634/document Project: https://creusot.rs ; repo https://github.com/creusot-rs/creusot ; user guide https://creusot-rs.github.io/creusot/guide/tutorial.html Underlying platform: Why3 / Coma (the new Creusot IR, replacing Why3's older WhyML emission path), targeting Z3, CVC5, Alt-Ergo 2.6.0 and others. Notable applications: CreuSAT (a verified SAT solver) and Sprout (a verified SMT solver), both Creusot case studies....

CompCert and the Verified-Compiler Toolchain

§1 Provenance Leroy. "Formal verification of a realistic compiler" , CACM 2009; full development https://compcert.org ; source https://github.com/AbsInt/CompCert ACM Software System Award 2022, ACM SIGPLAN Programming Languages Software Award. CompCertO line: Koenig & Shao, "CompCertO: Compiling Certified Open C Components" , PLDI 2021; Zhang, Wang, Wu, Koenig, Shao, "Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules" , POPL 2024. CompCertOC (PLDI 2025): verified compilation of multi-threaded...

Formal Models of the Rust Borrow Checker

§1 Provenance Jung, Dang, Kang, Dreyer. "Stacked Borrows: An Aliasing Model for Rust" , POPL 2020 / PACMPL 4. The original operational aliasing semantics for Rust. Villani, Hostert, Dreyer, Jung. "Tree Borrows" , PLDI 2025 / PACMPL 9 Article 188. https://dl.acm.org/doi/10.1145/3735592 ; PDF https://iris-project.org/pdfs/2025-pldi-treeborrows.pdf Distinguished Paper Award , PLDI 2025. Became the most-downloaded PACMPL paper of all time shortly after publication. Background blog: Jung, "From Stacks to Trees: A new...

Verus

§1 Provenance Lattuada, Hance, Cho, Brun, Subasinghe, Zhou, Howell, Parno, Hawblitzel. "Verus: Verifying Rust Programs using Linear Ghost Types" , OOPSLA 2023 (PACMPL 7). https://www.microsoft.com/en-us/research/publication/verus-verifying-rust-programs-using-linear-ghost-types/ Lattuada et al. "Verus: A Practical Foundation for Systems Verification" , SOSP 2024. https://dl.acm.org/doi/10.1145/3694715.3695952 ; PDF https://www.cs.utexas.edu/~hleblanc/pdfs/verus.pdf AutoVerus (Wang et al., OOPSLA October 2025), LLM-assisted proof generation. https://www.microsoft.com/en-us/research/publication/autoverus-automated-proof-generation-for-rust-code/ VeriStruct (Sun, Sun, Amrollahi, Zhang, Lahiri, Lu, Dill, Barrett, TACAS April 2026), AI-assisted verification of data-structure modules...

Formal Verification and Mechanized Safety

Capability-Machine Formalism and Endorsement Relations

§1 Provenance Cerise (logsem/cerise): Iris-based Coq mechanisation of a capability machine. https://github.com/logsem/cerise "Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code" , Journal of the ACM (JACM), 2023. https://dl.acm.org/doi/10.1145/3623510 Park, Pai et al. "A Formal CHERI-C Semantics for Verification" , TACAS 2023; "A CHERI C Memory Model for Verified Temporal Safety" , CPP 2025. CHERI hardware lineage: Watson et al., CHERI ISA reports, with hardware in...

CakeML and the Verified-JIT Line

§1 Provenance Kumar, Myreen, Norrish, Owens. "CakeML: a verified implementation of ML" , POPL 2014. https://dl.acm.org/doi/10.1145/2535838.2535841 Tan, Myreen, Kumar, et al. "A New Verified Compiler Backend for CakeML" , ICFP 2016. https://dl.acm.org/doi/10.1145/2951913.2951924 CakeML home: https://cakeml.org/ Myreen, PLDI 2024 keynote, "Much Still to Do in Compiler Verification (A Perspective from the CakeML Project)" . https://pldi24.sigplan.org/details/pldi-2024-papers/100/ Brack: A Verified Compiler for Scheme via CakeML by Lasnier, Yallop, Myreen, CPP 2026. https://popl26.sigplan.org/details/CPP-2026-papers/15/ FM-JIT...

Separation Logic for Managed (GC'd) Heaps

§1 Provenance McCreight et al. "GCSL: A logic for low-level programs with GC interfaces" (foundational, pre-Iris). https://ieeexplore.ieee.org/document/5970244/ Madiot & Pottier. "A Separation Logic for Heap Space under Garbage Collection" , POPL 2022 / PACMPL 6. https://dl.acm.org/doi/10.1145/3498672 ; PDF https://cambium.inria.fr/~fpottier/publis/madiot-pottier-diamonds-2022.pdf Charguéraud, Moine, Pottier. "A High-Level Separation Logic for Heap Space under Garbage Collection" , POPL 2023 / PACMPL 7. https://dl.acm.org/doi/10.1145/3571218 ; PDF https://www.chargueraud.org/research/2022/space_with_gc/space_with_gc.pdf Moine, Charguéraud, Pottier. "Will It Fit? Verifying Heap...

RustBelt and Iris

§1 Provenance Original paper: Jung, Jourdan, Krebbers, Dreyer. "RustBelt: Securing the Foundations of the Rust Programming Language" , POPL 2018 (PACMPL 2). https://dl.acm.org/doi/10.1145/3158154 Underlying logic: Jung, Krebbers, Jourdan, Bizjak, Birkedal, Dreyer. "Iris from the ground up" , JFP 2018; received the 2025 Most Influential POPL Paper Award and the 2023 Alonzo Church Award. Project home: https://plv.mpi-sws.org/rustbelt/ (MPI-SWS). The ERC RustBelt project formally ended April 2021 but the line continues. Major...

Aeneas

§1 Provenance Ho & Protzenko. "Aeneas: Rust verification by functional translation" , ICFP 2022 / PACMPL 6. https://dl.acm.org/doi/10.1145/3547647 ; arXiv https://arxiv.org/abs/2206.07185 Ho, Fromherz, Protzenko. "Sound Borrow-Checking for Rust via Symbolic Semantics" , ICFP 2024. https://icfp24.sigplan.org/details/icfp-2024-papers/17/Sound-Borrow-Checking-for-Rust-via-Symbolic-Semantics Project: https://github.com/AeneasVerif/aeneas (Inria + Microsoft Research). Frontend: Charon → LLBC. Backends: F*, Coq, HOL4, Lean (Lean is the maintainers' primary 2024-2026 target). Lean integration documentation: https://lean-lang.org/use-cases/aeneas/ Used in production: Microsoft's port of SymCrypt (the Windows...

20. Logic in Programming

Logic in programming studies how formal logic appears inside programming languages, program analysis, verification systems, and tools for constructing correct software. The chapter begins with logic programming, where programs are written as logical rules and computation proceeds by searching for proofs or satisfying assignments. Type systems are then introduced as logical disciplines for classifying programs, ruling out certain errors before execution, and expressing structural properties of data and functions. Verification...

20. Logic in Programming

Logic in programming studies how formal logic appears inside programming languages, program analysis, verification systems, and tools for constructing correct software. The chapter begins with logic programming, where programs are written as logical rules and computation proceeds by searching for proofs or satisfying assignments. Type systems are then introduced as logical disciplines for classifying programs, ruling out certain errors before execution, and expressing structural properties of data and functions. Verification...

09.5 Reproducibility and Verification

9.5 Reproducibility and Verification Computation is useful only when we can trust the result. If a calculation gives an answer, we should be able to ask two basic questions: can someone repeat the same computation, and can someone check that the result is correct? Reproducibility means that the same method gives the same result when repeated. Verification means checking that the method and the result are correct. Reproducibility Suppose a...