Formal Methods
- tags
- Math , Concurrency , Algorithms
Intro
- Different formalisms often have different ergonomics when it comes to different particular systems and properties, and the matter of personal aesthetic preference also plays a big role.
- At the end of the day, many those formalisms have similar expressivity (i.e., they can describe roughly the same set of systems and the same set of properties)
Theorem Provers and Formal Spec Tools
- Formal Logic
:
formal specification (description)+formal proof - Writing
formal specificationis different skillset from writingformal proofs. - You can write
formal specificationwithout knowing how to writeformal proof
| Name | Type |
|---|---|
| Alloy | Spec Tool |
| TLA+ | Spec Tool |
| Z3 | Model Checker |
| Lean | Proof Writing |
| Coq | Proof Writing |
| Isablle | Proof Writing |
Formal specification first
Temporal Logic of Action(TLA+)
- Good for specification of
order - TLA+ is a modelling/specification language for computational processes.
- Lamport’s hypothesis was that a programming language, no matter how simple, is still much more complicated and far less expressive than simple mathematics.
- Time is viewed as discrete (rather than continuous), considers branching time (as opposed to linear time) and in which time branches only into the future (and not into the past).
- Can be use to prove Paxos and Raft
- Can support Model checkers like Z3
- Resources
- Why I use TLA+ and not(TLA+): Episode 1 | Protocols Made Fun
- Specifying serializability in TLA+ – Surfing Complexity
- TLA from first principles • Buttondown
- An introduction to temporal logic and how it can be used to analyze concurrency | Hacker News
- An Introduction to TLA+ and Its Use in Parties | Lobsters
- Using TLA+ in the Real World to Understand a Glibc Bug
- https://medium.com/@polyglot_factotum/modelling-a-message-passing-bug-with-tla-baaf090a688d
- TLA+ in Practice and Theory<br/>Part 1: The Principles of TLA+
- TLA⁺ is more than a DSL for breadth-first search -
- A primer on formal verification and TLA+ — Jack Vanlightly
- Wrangling monotonic systems in TLA (See crdt )
Alloy
- Good for specification of
structure - Resources
Proof writing first
Lean and Coq are based on Lambda calculus
Lean
- Lean is a FP language and theorem prover that compiles to C
- Lean’s maths library is completely focused on classical mathematics
- From Z3 to Lean, Efficient Verification
- Logic and Proof — Logic and Proof 3.18.4 documentation
Coq
- Theorem Prover, Proof Assistant
- Learn Coq in Y Minutes
Model Checkers
SMT Solvers
Satisfiability Modulo Theories Solver
- SAT/SMT by Example (Book, Z3py)
- First-order logic - Wikipedia
- Learning 1: Reddit - Dive into anything
- Learning 2: Reddit - Dive into anything
Z3
Resources
- https://leanpub.com/logic?s=35 🌟
- Formal Methods: Just Good Engineering Practice? (2024) | Hacker News
- Formal Methods: Just Good Engineering Practice? - Marc’s Blog
- What I’ve Learned About Formal Methods In Half a Year — Jakob’s Personal Webpage
- PWLSF - 08/2014 - Peter Alvaro: Using Reasoning about Knowledge to Analyze Di…
- Logic and Algebras for Distributed Computing: Applications and Open Questions…