Erla+: Translating TLA+ Models into Executable Actor-Based Implementations
summary
Erla+ automatically converts a subset of PlusCal into runnable Erlang and a TLA+ model for TLC model checking, adding message-passing and failure primitives. The tool generates Erlang code that runs a Raft-based key-value store and passes the Yahoo Cloud Serving Benchmark; performance is competitive with a hand-written Raft library, outperforming it on some read-heavy workloads and falling about 20% behind at 16 threads, with saturation visible past 16–32 threads. The pipeline yields executable, debuggable implementations from verified models.
AI-written summary · about
chapters (9)
- 0:00ER Plus compiler intro
- 1:30Formal verification for distributed systems
- 4:47PlusCal modeling overview
- 6:36Bridging models and implementations
- 8:47ER Plus compiler workflow
- 10:55Extending PlusCal for actors
- 13:46Translating PlusCal to Erlang
- 17:44ER Plus real-world evaluation
- 22:48Summary and future work
related talks
01h 13mDesigning distributed systems with TLA+
01h 12mDistributed systems showdown — TLA + vs real code
34mTLA+ at Microsoft to build planetary-scale systems
01h 13mWorkshop: TLA+ in action (Part 3)
01h 12mWorkshop: TLA+ in action (Part 4)
35mDiving into Erlang is a one-way ticket
14mModel-guided Fuzzing of Distributed Systems
32mTLA + specification of PCR parallel programming pattern