Our great sponsors
-
-
tlaplus
TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
Regarding the last point — correct, Stateright aims to verify both.
It’s important to clarify that this doesn’t provide a proof of correctness, but it can dramatically improve confidence in both the design and implementation compared with fuzz testing, for example. This is done by exhaustively enumerating possible nondeterministic outcomes (e.g. due to message reordering) within specified constraints (e.g. up to S servers and C clients performing X operations…).
Examples:
SD Paxos: https://github.com/stateright/stateright/blob/master/example...
ABD (linearizable register algorithm): https://github.com/stateright/stateright/blob/master/example...
Imagine you are implementing a database engine and you want to make your database be able to run in run multiple nodes in order to make it fault-tolerant, therefore you need to implement some kind of consensus algorithm (Paxos, Raft) to select a leader and a followers, in case if some node fails, your entire cluster can keep working.
That said, implementing a consensus algorithm is quite hard. Modeling and testing is much harder, there is even a language just for this purpose; TLA+ [0].
[0]: https://lamport.azurewebsites.net/tla/tla.html
Related posts
- Ask HN: Usefulness of formal verification (Coq) and formal verification (TLA+)?
- Quint: A specification language based on the temporal logic of actions (TLA)
- Ask HN: How you understand TLA+ and how you use TLA+ in your projects?
- A collection of lock-free data structures written in standard C++11
- What I've Learned About Formal Methods in Half a Year