TLA+ Formal Verification
Discussions center on TLA+ as a formal specification language, its practical usefulness for verifying system designs especially in distributed systems, user experiences, limitations, and comparisons to tools like Coq, TLC, and PlusCal.
Activity Over Time
Top Contributors
Keywords
Sample Comments
TLA+ is basically an academic tool. It allows you to verify your specification, but it is useless to detect bugs in your implementation. In my experience, the process of writing your specification in TLA is a buggy enough process to make it all a waste of time.
Does anyone have any experience regarding TLA+. Does it make formal verification at least slightly less painful?
how does this relate to tools like TLA+? coq?
TLA+ is a specification language, not a verification language. There is currently no way of establishing correspondence between a TLA+ spec and the code you (presumably) write to implement that spec. There are benefits to this, like using TLA+ to spec the difficult parts of your system without having to buy the whole formal verification farm.
Can someone who has learned TLA+ comment on how useful it is has been for you?
The FAQ [0] clarifies some of what TLA+ is good for[0] https://learntla.com/intro/faq.html
TLA+ is mentioned a lot here and many people point out how it's practically infeasible to use it in real world systems. Just curious, is there any alternative to write specifications which are more closer to common programming languages and can be used by an average programmer to formally prove correctness?
Use TLA+ (which I thought they did)
TLA+ is not a model checker. It is a specification and proof language. However, it has verification tools that include a model checker (TLC) and a mechanical proof system (TLAPS), both support a large and useful subset of the language. There are also other TLA+ model checkers under development or already available with some effort. In many ways it is more similar to Coq and Isabelle than to Alloy. For one, it has proof of relative completeness: anything that can be proven about a system, can be
TLA+ is a formal specification language, not a model checker. There exists a model checker called TLC which works with TLA+. There also exists an associated proof system called TLAPS; TLAPS has been used to formally prove correctness of Byzantine Paxos.