Showing posts from June, 2022

Practical Tips on using TLA+ and P

TLA+ and P are formal specification languages that let us formally define the behavior of our system and have a model checker reason about its correctness. In this post, I want to share some practical tips on using these awesome tools. I am not going to explain the basics and I assumes the reader is already familiar with these languages. If you are not, you can learn more about TLA+ at  Leslie Lamport's website . For P, a great place to start is the official website . I also wrote a blog post on P that explains P with examples. TLA+ vs. P While both TLA+ and P are formal specification languages, they are used for different purposes. Proving vs. Testing The main difference between TLA+ and P is that TLA+ is used to  prove , while P is used to  test ,   the correctness. While both use model checking, only TLA+ is used for exhaustive model-checking where we explore all possible executions of a given specification. Thus,  when the model checker does not find a bug, you are guaranteed