TLA+
Formal verification · by Leslie Lamport
created · updated
A way to describe how a system behaves step by step so precisely that the description can be checked by a program, the way a blueprint is checked before construction. For example, a blueprint of a money transfer reveals that if a failure hits between the debit and the credit, money vanishes, and this is found before any code is written. The notation resembles mathematical formulas, so the entry step is higher than with Quint. The language was created by Leslie Lamport.
Source: Leslie Lamport’s TLA+ page
Where it appears · 4
- Vitest vs Jest · Specs and context
- How to find a race condition in code · Specs and context
- How model checking differs from testing · Specs and context
- TLA+ vs Alloy vs Quint · Specs and context