Model-based testing with TLA+ and Apalache
summary
Model-based testing uses TLA+ assertions and the Apalache model checker to auto-generate JSON counterexamples, transform them (via JSONata and tendermint-testgen) into static integration tests, and run them inside the normal cargo test flow. Models explore 4–7 validators and 3–5 blocks, find corner cases (less vs <=, future timestamps), and detect a real validator-ordering bug missed by standard tests. The pipeline increases coverage, keeps spec and code in sync, and produces executable failing cases with Apalache and model-based testing.
AI-written summary · about
chapters (12)
- 0:00Introduction to presenters
- 1:03Who is Informal Systems
- 4:04Tendermint Light Client overview
- 10:31Formalizing specs with TLA+
- 14:57Apalache model checker explained
- 18:54Standard testing drawbacks
- 20:46Model-based testing demo
- 22:57TLA+ test integration
- 24:26Counterexample to test conversion
- 26:16Results and bug findings
- 27:46Model-based testing benefits
- 28:29Future work and roadmap
related talks
24mTLA+: Your Secret Weapon Against Concurrency Hell
23mBeyond Tests What to Verify in AI Generated Code
30mTackling Concurrency Bugs with TLA+
44mModel-Based Testing for the Zephyr RTOS
43mCan you Test it
47mTDD & Generative AI: A Perfect Pairing
23m„Complete” In-Sprint Testing Using Collaborative Models
23mHUSTEF 2014 - Stephan Schulz