TLA+ is a formal specification language used to model software systems. We can take the specification and check if it satisfies the properties we want, or produce a counterexample if it doesn’t. TLA+ is exceptionally well-suited for specifying concurrent and distributed systems, everything from kernel spinlocks to communicating microservices.
TLA+ is my specialty. I’ve written numerous articles and two guides, the Practical TLA+ book and the learntla free website. I also offer consulting services.
- Related Tags
-
- Alloy: Another formal method I specialize in.
- Formal Methods: The general discipline that TLA+ falls under.
- Case Study Highlights
-
- Augmenting Agile With Formal Methods: Taking a software bug that resisted the testing efforts of several Extreme Programming experts and cracking it in just over half an hour.
- Finding Goroutine Bugs with TLA+: Based on Even in Go, concurrency is still not easy. Reproducing the example Go bug in TLA+ and verifying all of the proposed fixes also work.
- Designing Distributed Systems With TLA+: Video. My standard conference talk on the applications of TLA+ to designing large scale systems.
- Blub Studies
-
- TLA+ Action Properties: How to write properties on the transitions on states, such as “this log grows monotonically”.
- Weak and Strong Fairness: Introducing the two ideas and how to use them in specifications.
- Modeling Message Queues with TLA+: Various approaches to specifying message queues.
- Modeling Adversaries with TLA+: How to model external or environmental forces in your spec.