Proof layer
Formal methods with TLA+
Write TLA+ specs that catch concurrency bugs before any code exists.
- 01
Why tests are not enough
The bug that needs 3 messages in one exact order.
- 02
Systems as state machines
States, steps and behaviours.
- 03
Your first TLA+ spec
A transfer between two accounts, checked by TLC.
- 04
Invariants
Things that must be true in every state.
- 05
Liveness
Things that must happen eventually.
- 06
Modeling retries and duplicates
Let the checker deliver every message twice.
- 07
Specifying a ledger
Prove money is never created or lost.
- 08
Property-based testing
Check the code against the spec's rules.
- 09
Deterministic simulation testing
Replay any failure, exactly.