HN Books @HNBooksMonth

This question is difficult to answer in general, because TLA+ is a very particular kind of formal verification tool (it's a model checker designed more around concurrent hardware/software than e.g. pure mathematics or general proving, or equivalence checking, etc). There are a lot of verification tools out there, many of them substantially different in scope, intent, and design. It's a bit like asking "What prerequisites do I need to drive a (boat or a motorcycle)?" They're very different beasts, and it's a very big field.

On this note, "non-trivial" formal verification can often be very, very non-trivial, depending on how you approach it. And I mean that in the sense that actually writing the specifications and proving them can be extremely hard, depending on the tools -- even if the problem itself may 'seem' easy. Think "I have a 1000 line program that needs 10,000 lines of proofs". (1-2 orders of magnitude is probably a good ballpark estimate, if you're doing things with tools like Coq.)

Luckily, TLA+ in particular is pretty easy to learn and you can get productive in a few weeks I think, and it's geared more towards engineers than e.g. general mathematicians or whatever. This introduction is pretty good:

  - https://learntla.com/introduction/

If you want a more general background... Go pick up some books on logic and computability. The things you learn here will apply deeply to nearly every approach to formal verification you can think of. Start with simple propositional logic, and you can move up to first-order logic, higher-order logics or type theory later on. This will help you understand logical systems, how to prove propositions, their relations, what can be decided etc, which will be deeply useful, forever.

If you want the book on this stuff, I strongly recommend the following one. It is dense but it is, in short, the bible of automated computer-based theorem proving, as far as I'm concerned, and has substantial code to back it up. (The author does formal verification of FPUs at Intel):

https://www.amazon.com/Handbook-Practical-Logic-Automated-Re...

⬐ pron

I agree with almost everything you say, but I have a few comments.

First, TLA+ is not a model checker. It is a specification and proof language that also has tools in the form of a model checker (more than one, actually) and a mechanical proof system.

Second, it is absolutely true that TLA+'s focus is not general mathematical theorem proving, and its intended audience are engineers, but it is not so much designed around concurrent hardware/software but that it is designed for algorithms in general. This means that it is also very appropriate for reasoning about concurrent or interactive (which is just a form of concurrency), whereas general mathematical tools that are often designed to reason about constructive functions rather than algorithms, and so can naturally reason about sequential algorithms, but need extra effort to reason about interaction or concurrency.

Finally, a strong focus of TLA+ is that it can serve as a refinement calculus, namely reason about the same system/algorithm at different abstraction levels, and explore the precise relationship between the different levels.

I agree that TLA+'s most practical advantage is that for its power, it is exceptionally easy to learn and apply in practice (much of this is due to the availability of a model checker). I also agree that ultimately, the specification, reasoning, and proof work in pretty much all formal tools is much more similar than different.

The author of this book is John Harrison of Intel, where his knowledge of automatic proofs is used in optimally designing chipsets. He is also the author of HOL Light (http://www.cl.cam.ac.uk/~jrh13/hol-light/), a program that helps users prove mathematical theorems. The submission is a book that he published in 2009 describing automated proofs, with a full implementation in OCaml. When I was doing grad work back in 2007-2008, the source code that went along with this book was invaluable in my work. I'm surprised that I haven't seen much discussion about this book, which is definitely worth checking out.

Amazon has a few good reviews (http://www.amazon.com/Handbook-Practical-Logic-Automated-Rea...), and a CMU faculty member wrote an extensive review (http://www.andrew.cmu.edu/user/avigad/Reviews/harrison.pdf).