3 ms·
TLA+ allows you to encode your system as a state machine, define invariants that must always be true, and the checker will explore your state machine and verify
by gamegoblin 7y ago
TLA+ allows you to encode your system as a state machine, define invariants that must always be true, and the checker will explore your state machine and verify that the invariants are always true.
An example would be encoding a distributed locking system, with an invariant saying "no lock is owned by more than 1 node at a time". You would encode all of the locking and unlocking behavior in your state machine, and then the checker would verify it.
- jsjolen 7y agoSo to ensure that your system follows this state machine you need to write a proof for that in some other theory (like an abstract interpretaion of your program)?
- dwohnitmok 7y agoIn theory (no pun intended) yes. In practice this is not done. Perhaps never done. I know of only one toy example that you could maybe extend to do this. TLA+ is meant to double-check design level questions and intuitions rather than code level or implementation level ones. That is it attempts to give guidance on whether a design is flawed rather than whether an implementation successfully follows a specified design. This may sound limiting, but the fact that this is an artifact completely separate from code makes TLA+ much more attractive from a business risk perspective in my opinion.