Hacker News Reader

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.

View on HN

So 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)?

In 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.

Reply on news.ycombinator.com