AWS used TLA+ to find subtle bugs in S3, DynamoDB, and other core services. These bugs would never have been found through testing, and could have caused data loss in production.
How Formal Verification Works
You write a model, a mathematical abstraction of your system. The model captures the essential behavior you care about while ignoring irrelevant details. A model checker then exhaustively explores every possible state of this model, checking your properties against each one. This is fundamentally different from testing. Testing checks specific scenarios you thought to write. Model checking explores the entire state space. AWS found a 35-step bug in DynamoDB that escaped all their tests and two code reviews. The model checker found it because it explored paths no human thought to test.The Model Must Be Accurate
When a model checker reports “no violations found,” it means the properties hold in your model. If your model accurately represents the real system, you gain confidence. If your model diverges from reality, bugs can hide in the gap. A 2016 study by Fonseca et al. examined three formally verified distributed systems: Iron Fleet, Verdi, and Chapar. They found 16 bugs through testing and code review. The results were instructive:- Zero protocol-level bugs. The verification worked. The core distributed algorithms were correct.
- 11 bugs in the shim layer. The interface between verified and unverified code, where assumptions about the operating system and network were encoded, contained most issues.
Abstraction Is a Tradeoff
Abstraction makes verification tractable. Real systems have infinite or astronomically large state spaces. By abstracting away details, we reduce the state space to something a model checker can explore. The seL4 microkernel, among the most thoroughly verified software ever created, explicitly documents what it assumes: assembly code correctness, boot code behavior, hardware functioning per specification, and more. This honestly is brilliant. The verification is real and valuable. But the team explicitly delineates where the proof ends and trust begins.Learning Paths
Two complementary approaches, each with a learning progression from basics to real-world application.TLA+
TLA+ models systems as state machines and verifies temporal properties: what happens over sequences of operations.TLA+ Basics
Gentle introduction for beginners. Build a light switch, then find a concurrency bug in a bank transfer system.
TLA+ Syntax Guide
Complete language reference. Set theory, operators, temporal logic, and common patterns.
Alloy
Alloy analyzes structural properties and finds counterexamples: specific configurations that violate your assertions. Alloy 6 added temporal operators, enabling behavioral verification similar to TLA+.Alloy Basics
Gentle introduction for beginners. Model a file system, then discover a permission bug when files move between folders.
Alloy Syntax Guide
Complete language reference including Alloy 6 temporal features, relational operators, and common patterns.
When to Use Which
| Aspect | TLA+ | Alloy |
|---|---|---|
| Focus | Behavior over time | Structure (temporal in Alloy 6+) |
| Question | ”Does this sequence of operations stay safe?" | "Can this bad configuration exist?” |
| Verification | Model checking (exhaustive state exploration) | SAT solving (constraint satisfaction) |
| Strength | Protocols, concurrency, distributed systems | Data models, permissions, access control |
| Output | Counterexample traces (sequences of states) | Counterexample instances (specific configurations) |
Native macOS Tools
Running formal verification traditionally requires Java-based tools. I built native macOS alternatives that run locally:MacTLA
Native TLA+ IDE with built-in model checking, PlusCal translation, and interactive state visualization.
MacAlloy
Native Alloy 6.2 IDE with built-in CDCL SAT solver and force-directed instance visualization.
Domain Applications
Formal methods applied to specific domains, from security to safety-critical systems.Active Directory Security
Verify that AD tier models prevent credential theft and privilege escalation. Mathematically prove no attack paths exist.AD TLA+ Specification
Example specification reviewing Active Directory, temporal verification of tier isolation. 10 safety invariants covering credential protection and state transitions.
AD Alloy Specification
Example specification reviewing Active Directory, for structural analysis of ACLs for attack paths. 11 predicates covering DCSync, RBCD abuse, Shadow Credentials, and more.
Binary Analysis
Formal methods for reverse engineering and vulnerability research. Constraint solving meets binary analysis.Formal Methods for Binary Analysis
Three-part series covering SAT/SMT solvers, symbolic execution, and practical applications in malware analysis and exploit development.