Introduction
Glossary, Resources
1.
Foundations
1.1.
Paradoxes
1.2.
Incompleteness, Undecidability, Inconsistency
1.3.
Computability and Lambda Calculus
1.4.
Propositions as Types: The First Correspondence
1.5.
Church Encodings
1.6.
Lambda Cube
1.7.
Propositions as Types: More Incarnations
1.7.1.
System F and the Polymorphic Lambda Calculus
1.7.2.
Modal Logic and Monads
1.8.
HoTT
2.
Dependently Typed Languages
2.1.
Idris
2.2.
Coq
2.3.
Lean
2.4.
Agda
2.5.
Isabelle/HOL
2.6.
F*
3.
SMT Solvers
3.1.
Theory and Implementation
4.
Model Checking
5.
Full Applications
5.1.
Verifying Rust with Verus
5.1.1.
Verus Fundamentals
5.1.2.
Borrow Checker, Linear Types
5.1.3.
Case Study: Verified Parsers
5.2.
Verified Cryptography
5.2.1.
Cryptol for Haskell Knowers
5.2.2.
Cryptol for Anyone
5.2.3.
Cryptol + Saw
5.3.
Verified Hardware with SystemVerilog
Light (default)
Rust
Coal
Navy
Ayu
A Journey Through Formal Methods
Verifying_Rust_With_Verus