Formal Methods
Table of Contents
- A Map
- General formal methods
- Theorem proving
- Formal specification
- Formal methods in Rust
- Formal verification
- Compiler verification
A Map
graph LR;
FormalModel;
FormalMethod;
FormalSpecification;
FormalVerification;
Logic;
ModalLogic;
TemporalLogic;
LogicProgramming;
ConstraintLogicProgramming;
AutomaticTheoremProving;
ProofAssistant;
ModelChecker;
SAT;
3SAT;
SMT;
Types;
Coq;
Agda;
Idris;
Lean;
Alloy;
TLAPlus;
PlusCal;
Z3;
Prolog;
Datalog;
MiniKanren;
Souffle;
Creusot;
Logic-->ModalLogic;
ModalLogic-->TemporalLogic;
TemporalLogic-->TLAPlus;
Logic-->Types;
Logic-->ProofAssistant;
Logic-->SAT;
Types-->CategoryTheory;
ProofAssistant-->Lean;
SAT-->Z3;
ModelChecker-->TLAPlus;
ModelChecker-->Alloy;
TLAPLus-->PlusCall;
LogicProgramming-->Prolog;
LogicProgramming-->Datalog;
LogicProgramming-->MiniKanren;
General formal methods
- Wikipedia: Verification and validation
- ⚠️ Wikipedia: Software verification and validation
- ⚠️ Wikipedia: Formal verification
- ⚠️ Wikipedia: Formal methods
- ⚠️ Wikipedia: Formal specification
- Verdi Formally Verifying Distributed Systems
- Github: awesomo4000/awesome-provable A curated set of links to formal methods involving provable code.
- Everything I Know - Formal verification
- Formal Methods Wiki
- Software Foundations
- ⚠️ Resources for Teaching with Formal Methods
- Formal Reasoning About Programs
- Verdi: Formally Verifying Distributed Systems
- Formality: A modern programming language featuring formal proofs
- 1999/03 High-Quality Software Through Semiformal Specification and Verification
- 2016/09 Wired: Computer Scientists Close In on Perfect, Hack-Proof Code
- 2017/11 Lobste.rs: Your thoughts on this advice to those pursuing formal methods?
- 2017/11 Writing Code like a Mathematical Proof
- 2017/11 My hobby: proof engineering
- 2017/12 Formal Verification: The Gap Between Perfect Code and Reality
- 2018/10 Formally Verified Software in the Real World
- 2019/01 ⚠️ Hillel Wayne: Why Don't People Use Formal Methods? L.rs HN
- 2019/01 Utterly Unpersuasive: Formal Methods and Law HN
- 2019/01 Modeling in Engineering and Science
- 2019/02 Lobste.rs: Program synthesis of a spec with optional manual implementation for parts of the program
- 2019/03 What, Why, and How of Formal Methods
- 2019/03 ⚠️ Hillel Wayne: Using Formal Methods at Work
- 2019/04 Explaining formal proofs
- 2019/12 A mathematical formulation of the tax code?
- 2020 The 2020 Expert Survey on Formal Methods
- 2020/01 ⚠️ Hillel Wayne: The Business Case for Formal Methods
- 2020/02 ZetZ is a Formally Verified Dialect of C
- 2020/02 ⚠️ Formal Methods: From Academia to Industrial Practice. A Travel Guide
- 2020/07 Formal Software Verification Measures Up
- 2020/07 ⚠️ PLTalk: Practical Formal Methods with Hillel Wayne
- 2020/08 Hillel Wayne: How knowing math helps you write better software
- 2020/04 ⚠️ Hillel Wayne: A Very Brief Intro to Formal Methods (aka my job)
- 2020/05 Formal Verification: History and Methods
- 2020/12 Coding as a tool of thought
- 2021/04 Hillel Wayne: Why UML "Really" Died
- 2021/04 Hillel Wayne: Can Formal Methods Succeed where UML Failed?
- 2021/07 Program Verification: Vision and Reality
- 2021/07 ⚠️ Hillel Wayne: 10 Misconceptions about Formal Methods
- 2021/09 ⚠️ Lobste.rs: Is the formal methods winter about to end?
- 2021/10 You Already Know Formal Methods HN
- 2021/10 Using lightweight formal methods to validate a key-value storage node in Amazon S3
- 2022/04 Proving the Coding Interview Part 1
- 2022/04 Proving the Coding Interview Part 2
- 2022/04 Proving the Coding Interview Part 3
- 2022/06 Formal Methods Only Solve Half My Problems L.rs
- 2022/07 The Verification Gap: A Major Hurdle for the Industry Adoption of Formal Methods L.rs
Videos
- 2019/11 Formal Methods of Software Design
- 2020/06 Kathleen Fisher: Using Formal Methods to Eliminate Exploitable Bugs
Theorem proving
Coq
- Wikipedia: Coq
- Official website
- Github: Coq
- Learn X in Y minutes Where X=Coq
- Certified Programming with Dependent Types
- Coq'Art Home page
- 2020/11 Untangling mechanized proofs HN
Agda
- Official website
- Wikipedia: Agda (programming language)
- Learn You an Agda and achieve enlightenment
- Agda Tutorial
- 2013/02 Brutal [Meta]Introduction to Dependent Types in Agda
- 2018/11 Constructive and Non-Constructive Proofs in Agda (Part 1): Logical Background
- 2018/11 Constructive and Non-Constructive Proofs in Agda (Part 2): Agda in a Nutshell
- 2018/11 Constructive and Non-Constructive Proofs in Agda (Part 3): Playing with Negation
- 2019/03 Introduction to Univalent Foundations of Mathematics with Agda
- 2020/02 ⚠️ Agda vs. Coq vs. Idris
Videos
Formal specification
- 2020/08 ⚠️ Hillel Wayne: Formal Specification Languages
- DeepSpec: The science of deep specification
- RISC Algorithm Language The RISC Algorithm Language (RISCAL) is a specification language and associated software system for describing mathematical algorithms, formally specifying their behavior based on mathematical theories, and validating the correctness of algorithms, specifications, and theories by execution/evaluation.
Alloy
- Alloy
- Github: Alloy
- Guide to Alloy
- Wikipedia: Alloy
- Alloy 6
- 2018/05 State Machines and Alloy
- 2019/02 Validating a Coordination Protocol with Alloy
- 2022/01 ⚠️ Formal modeling as a design tool
- 2020/04 Hillel Wayne: Announcing: Alloydocs
- 2021/11 ⚠️ Alloy 6 First Impressions
- 2021/11 Alloy 6: it's about Time
- 2021/05 Modelling data pipelines with Alloy
- 2021/12 Learning DNS by modeling it with Alloy
Videos
- 2019/10 Alloy for TLA+ users - Jay Parlar
- 2019/11 "Finding bugs without running or even looking at code" by Jay Parlar
TLA+
- ⚠️ TLA+ Basics Tutorials
- TLA+ Cheatsheet
- ⚠️ Apalache Documentation: Idiomatic TLA+ Apalache is a symbolic model checker for the specification language TLA+
- TLA+ Conf
- reddit.com/r/tlaplus/
- Introduction to Pragmatic Formal Modeling
- 2021/08
afonsonf/tlaplus-graph-explorerA static web application to explore and animate a TLA+ state graph. - 2022/05
informalsystems/modelator-pyUtilities for the TLA+ ecoystem and model-based testing using TLA+.
Leslie Lamport:
- TLA home page
tlaplusGithub Org- Wikipedia: TLA+
- Wikipedia: PlusCal
- Leslie Lamport: The specification language TLA+
- Leslie Lamport: Summary of TLA+
- Leslie Lamport: A summary of TLA+
- The TLA+ Hyperbook
- PlusCal Tutorial
- 1999/06 Model Checking TLA+ Specifications
- 2018/07 ⚠️ Leslie Lamport: If You’re Not Writing a Program, Don't Use a Programming Language
- 2022/05 Q&A How to Write Software With Mathematical Perfection
Hillel Wayne: Twitter Blog Github
- Learn TLA+
- 2017/03 Formal Methods in Practice: Using TLA+ at eSpark Learning
- 2018/02 Modeling Redux with TLA+
- 2018/03 List of TLA+ Examples
- 2018/10 Practical TLA+ Now Available
- 2018/10 Modeling Message Queues in TLA+
- 2019/04 ⚠️ The Case for Formal Methods
- 2020/09 Finding Goroutine Bugs with TLA+
- 2020/10 Edge Case Poisoning
- 2021/02 TLA+ Action Properties
- 2021/04 ⚠️ Why Specifications Don't Compose
- 2021/12 ⚠️ Using Abstract Data Types in TLA+
- 2022/07 Announcing: Learn TLA+ l.rs
- 2015/01 ⚠️ My experience with using TLA+ in distributed systems class
- 2018/01 ⚠️ Why you should use modeling [with TLA+/PlusCal]
- 2018/07 ⚠️ Metadata: If You’re Not Writing a Program, Don't Use a Programming Language
- 2018/08 TLA+ specification of the consistent prefix guarantee
- 2018/10 ⚠️ Debugging designs with TLA+
- 2019/01 Building a "Simple" Distributed System - The What
- 2019/01 Building A "Simple" Distributed System - The Protocol
- 2019/01 Building A "Simple" Distributed System - Formal Verification
- 2021/12
Vanlightly/bookkeeper-tlaplusA TLA+ specification of the Apache BookKeeper replication protocol
Lorin Hochstein: Twitter Blog Github
- 2017/10 The Tortoise and the Hare in TLA+
- 2018/12 TLA+ is hard to learn HN
- 2018/12 Inductive invariants
- 2017/05 ⚠️ TLA+ in Practice and Theory Part 1: The Principles of TLA+
- 2017/06 ⚠️ TLA+ in Practice and Theory Part 2: The + in TLA+
- 2017/06 ⚠️ TLA+ in Practice and Theory Part 3: The (Temporal) Logic of Actions HN
- 2017/06 ⚠️ TLA+ in Practice and Theory Part 4: Order in TLA+
Markus Kuppe:
- 2018/07 State Space Explosion or: How To Fight An Uphill Battle
- 2014/06 Distributed TLC - TLA+ Community Event 2014, Toulouse
- 2015/04 Cloud distributed TLC
- 2016/11 Install TLA+Toolbox on Ubuntu from APT repository
- 2016/11 TLA+ Toolbox for Beginners
- 2018/04 Large Scale Model Checking 101
- 2018/04 Large Scale Model Checking 101 - Addendum “Views”
Other:
- 2013/01 Exploring TLA+ with two-phase commit
- 2015/04 ⚠️ How Amazon Web Services Uses Formal Methods
- 2015/04 Specifying and Verifying Concurrent C Programs with TLA+
- 2017/01 An Example of Debugging Java with a Model Checker
- 2017/03 Solving the Water Jug Problem from Die Hard 3 with TLA+ and Hypothesis
- 2017/07 Solving the “Wolf, Sheep and Cabbage” problem using TLA+ and the TLC model checker
- 2017/04 Getting Started With TLA+
- 2019/01 Using TLA+ to Understand Xen Vchan
- 2019/01 ⚠️ Introduction to TLA+ Model Checking in the Command Line
- 2019/04 ⚠️ A beginner's experience with TLAPS (The TLA+ Proof System)
- 2019/04 Using TLA+ to Model Cascading Failures
- 2019/10 TLA+ Model Checking Made Symbolic
- 2019/11 TLA+ for startups (part 1)
- 2019/12 TLA+ for startups (part 2)
- 2019/12 Train Sidings – A TLA+ Example
- 2019/09 2019 TLA+ Conf
- 2020/05 TLA+ on OpenBSD
- 2020/05 Specifying and Model Checking Workflows of Single Page Applications with TLA+
- 2020/06 Breaking state channels with TLA+ -
statechannels/tla-specsTLA+ specifications of various protocols used by wallets in the nitro protocol - 2020/07 TLA+ specification of the parser for BIP32 path templates
- 2020/09 Voucher System verification using TLA+
- 2020/10 Using TLA+ in the Real World to Understand a Glibc Bug HN
- 2020/11 Specifying a simple serverless system with TLA+ r/
- 2021/07 Github: mitchellh/tlaplus-radix-tree TLA+ modules, specifications, and models for Radix trees
- 2021/08 Github: afonsonf/tlaplus-graph-explorer A static web application to explore and animate a TLA+ state graph
- 2021/09 r/tlaplus: Why TLA+ Is Untyped
- 2021/10 Current and Future Tools for Interactive TLA+
- 2022/01 TLA+: The Best Debugger/ Optimizer You’ve Never Heard of
- 2022/06 Modelling the archetype of a message-passing bug with TLA+
TLA+ and consensus algorithms
- Github: TLA+ Consensus Specifications
- Github: tlaplus/DrTLAPlus Dr. TLA+ series - learn an algorithm and protocol, study a specification
- Github: Starydark/Tencent-Paxos-TLA Specification of the consensus algorithm in Tencent storage system PaxosStore
- Github: ongardie/raft.tla TLA+ specification for the Raft consensus algorithm
- Github: afonsonf/ceph-consensus-spec TLA+ specification of the Ceph consensus algorithm
- 2007 Asynchronous Consensus: A Model in TLA+
- 2018 ⚠️ Consensus Protocol Using TLA+
- 2019/10 Formal Analysis of the CBC Casper Consensus Algorithm with TLA+
- 2021 ⚠️ Verification and Visualization of a Consensus Algorithm using TLA+
Videos
- 2017/06 Curry On Talk: The Practice and Theory of TLA+
- 2017/06 Ron Pressler - The Practice and Theory of TLA+
- 2018/07 Applying TLA+ in a Safety-Critical Railway Project - Stefan Resch
- 2018/12 Lightning Talk: Formally Verifying Complex Systems Using TLA+ 2019/04 Pawel Szulc - Formal verification applied (with TLA+)
- 2019/09 Exposing Design Flaws in Shared-Clock Systems with TLA+ - Russell Mull
- 2019/09 Using TLA+ for fun and profit in the development of Elasticsearch - Yannick Welsch
- 2020/04 A gentle intro to TLA+
- 2021/12 A Beginner's Guide to TLA+ Exploring State Machines & Proving Correctness | Jeff Weiss | Code BEAM V
- 2020/12 SREcon20 Americas - Weeks of Debugging Can Save You Hours of TLA+
- 2020/12 Dharma Shukla: TLA+ at Microsoft to build planetary-scale systems - Keynote TLA+ Community Event
- Markus Kuppe: TLA+ Toolbox for Beginners
Leslie Lamport:
- Leslie Lamport's TLA+ Video Course
- The TLA+ Video Course
- 2014/07 Thinking Above the Code
- 2016/09 “The PlusCal Algorithm Language”
- 2017/03 Why Don't Computer Scientists Learn Math?
- 2019/10 What's the difference between programming and coding
- 2019/10 How to think clearly as a programmer with mathematics and TLA+
Hillel Wayne:
- 2017/10 "Tackling Concurrency Bugs with TLA+"
- 2018/11 Designing Distributed Systems with TLA+
- 2018/12 Designing Distributed Systems with TLA+
- 2018/12 Everything about distributed systems is terrible
- 2019/04 Designing Distributed Systems with TLA+
- 2020/02 YOW! 2019 Designing Distributed Systems with TLA+
- 2020/11 Designing distributed systems with TLA+
- 2020/12 The Future of Formal Methods
- 2021/02 Hillel Wayne is Designing Distributed Systems with TLA+
- 2021/09 Strange Loop Chat with Hillel Wayne about TLA+
- 2021/10 TLA+ Tiramisu
Books
Leslie Lamport - Specifying Systems
- I Getting started
- 1 A little simple math
- 2 Specifying a simple clock
- 3 An asynchronous interface
- 4 A FIFO
- 5 A caching memory
- 6 Some more math
- 7 Writing a specification: some advice
- II More advanced topics
- 8 Liveness and fairness
- 9 Real time
- 10 Composing specifications
- 11 Advanced examples
- III The tools
- 12 The syntactic analyzer
- 13 The TLATEX typesetter
- 14 The TLC model checker
- IV The TLA+ language
- 15 The syntax of TLA+
- 16 The operators of TLA+
- 17 The meaning of a module
- 18 The standard modules
Practical TLA+
-
Part I The Semantics of TLA+ and PlusCal
- 1 An example
- 2 PlusCal
- 3 Operators and Functions
- 4 Constants, Models and Imports
- 5 Concurrency
- 6 Temporal Logic
-
Part II Applying TLA+
- 7 Algorithms
- 8 Data Structures
- 9 State Machines
- 10 Business Logic
- 11 MapReduce
- A Math
- B The PT Module
- C PlusCal to TLA+
Quickstrom
Formal methods in Rust
- Rust Formal Methods Interest Group
- Github: rust-formal-methods/wg
- Rustc Verification Working Group
- Github: rust-lang-nursery/wg-verification
- Github: PolySync/misra-rust An investigation into what adhering to each MISRA-C rule looks like in Rust. The intention is to decipher how much we "get for free" from the Rust compiler.
- Github: xldenis/creuso deductive verification of Rust code. (semi) automatically prove your code satisfies your specifications!
- 2021/05 Rust Verification Workshop 2021
- 2021/10 Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3
- 2022/08 hn
- https://github.com/viperproject/prusti-dev
- https://news.ycombinator.com/item?id=33190973
Ralf Jung
Alastair Reed Blog
High Assurance Rust
RustBelt
- RustBelt
- 2015/10 Formalizing Rust
- 2019/09 RustBelt: Logical Foundations for the Future of Safe Systems Programming
Ferrocene
Kani
- The Kani Rust Verifier
- Github
- 2022/05 Verifying Dynamic Trait Objects in Rust
- 2022/04 Announcing the Kani Rust Verifier Project
- 2022/06 Using the Kani Rust Verifier on a Rust Standard Library CVE
- 2022/07 Using the Kani Rust Verifier on a Firecracker Example
Magmide
- GithubA dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
TLA and Rust
- 2017/05 GitHub: spacejam/tla-rust: writing correct lock-free and distributed stateful systems in Rust, assisted by TLA+
- ⚠️ 2020/04 Rust, TLA+, Aesthetics and more
Formal verification
Videos
- Basics of Program Verification (ft. Viktor Kuncak)
- Planning Out Verification
- An introduction to Formal Verification Part 1
- An introduction to Formal Verification Part 2
- Getting started with Formal Verification Part 1: Introduction and Solvers
Model checking
Videos
- 2007 Edmund M. Clarke, ACM A.M. Turing Award Lecture "Model checking"
- 2017/09 Model Checking Course
- 2021/09 Model Checking Course
- 2020/08 Formal Methods for Verification and Model Checking
Compiler verification
- Wikipedia: Compiler correctness
- 2013/01 An Introduction to Compiler Verification
- 2021/06 Verifying a Quantum Compiler
- 2022/02 Reddit: Compiler Verification Engineer -- Is this role good for a new grad trying to be a SWE?
CompCert
Videos
- 2015/03 Compiler verification for fun and profit
- 2016/06 Using a Push-Button Verifying Compiler to Build Verified Software Components
- 2018/12 On the Architecture of a (Verifying) Compiler
- 2019/03 Galois, Inc. Tech Talk: Goldilocks the verification engineer
- 2019/10 [PurPL Fest] Compiler Verification: The Next Generation - Amal Ahmed
- 2020/01 Verification and Validation Process (V&V Curve)
- 2021/01 Nomadic Labs Research Seminars #6 | Towards mechanised verification of the LIGO compiler
- 2021/06 Can you trust your compiler? — With CompCert, you can!