Formal Methods

A Map
General formal methods
- Videos
Theorem proving
- Coq
- Agda
  - Videos
Formal specification
Formal methods in Rust
- High Assurance Rust
- RustBelt
- Ferrocene
- Kani
- Magmide
- TLA and Rust
- Hacspec
Formal verification
- Videos
- Model checking
  - Videos
Compiler verification
- CompCert
  - Videos

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

Wikipedia: Proof assistant

Coq

Agda

Videos

Introduction to Agda

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-explorer A static web application to explore and animate a TLA+ state graph.
2022/05 informalsystems/modelator-py Utilities for the TLA+ ecoystem and model-based testing using TLA+.

Leslie Lamport:

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

Murat Demirbas: Twitter Blog

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+

Jack Vanlightly: Twitter Blog

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-tlaplus A 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

Ron Pressler: Twitter, Blog

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
- Compiling Distributed System Models into Implementations with PGo
- S-expressions for Actions with Logic Temporal
- Exposing Design Flaws in Shared-Clock Systems using TLA+
- Fixing a MongoDB Replication Protocol Bug with TLA+
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-specs TLA+ 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
- ⚠️ Dr. TLA+ Series- Paxos
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

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+

2019/05 Book Review: 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
- Hacker News Comments
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
- Talks
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

Ferrocene

2022/06 Introducing the Ferrocene Language Specification
- r/

Kani

The Kani Rust Verifier
Github
- Hacker News Comments
2022/05 Verifying Dynamic Trait Objects in Rust
- Reddit Comments
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.
- Hacker News Comments

PKB

Formal Methods

Table of Contents

A Map

General formal methods

Videos

Theorem proving

Coq

Agda

Videos

Formal specification

Alloy

Videos

TLA+

TLA+ and consensus algorithms

Videos

Books

Leslie Lamport - Specifying Systems

Practical TLA+

Quickstrom

Formal methods in Rust

High Assurance Rust

RustBelt

Ferrocene

Kani

Magmide

TLA and Rust

Hacspec

Formal verification

Videos

Model checking

Videos

Compiler verification

CompCert

Videos