The Paxos Algorithm, or How to Win a Turing Award

The largest programs ever verified end-to-end with Coq, Isabelle, or any other proof assistant correspond to about ~10KLOC of C, or less than 1/5 of jQuery (although such a small program could require up to 50K or even 100K lines of proofs). And even those certainly-non-trivial-yet-rather-tiny programs took years of efforts by experts. Moreover, concessions in the programs' design and choice of algorithms had to be made in order to make verification feasible at all.

And I agree that extraction doesn't suffer from a scalability problem. What does is the ability to verify the spec in the first place. If we could write proofs that correspond to programs with 100K, then extracting an executable would not be the isse, but we can't (or, at least, we don't know how).

> Is it really true that TLA scales to large programs?

Yes. Again, there's no magic: we can only verify so many lines of a formal spec (of which code is an example). So it's either a small program or a small high-level spec that corresponds to a large program. No known technique can affordably verify large (or even medium, or even non-small) programs, end-to-end, for arbitrary functional correctness properties.

> Why isn't there a Compcert in TLA?

There are programs fifty times the size of CompCert that used TLA+ (to be honest, most real-world programs are 50x the size of CompCert), but not for end-to-end verification; i.e. there is an informal translation of spec to code. Unlike Coq, which is usually used for research or by researchers, TLA+ is used in industry and by "ordinary" engineers without lengthy training in formal logic, so there aren't many papers written about its use, but here's one[1]. Ironically, another reason you don't see as many papers about verification in TLA+ as in Coq is that its use is much simpler. I once saw a paper about specifying and verifying a program's time-complexity in Coq. No one would ever write such a paper about TLA+, because it's just too easy; a TLA+ beginner could do it in their first week of learning (the main reason there's a paper about using TLA+ for PharOS is because they used TLAPS, the TLA+ proof assistant, rather than the TLC model checker, which made the work academically interesting).

In any event, if someone is interested in using any of those tools "in production," I recommend they give them all a try.

[1]: https://members.loria.fr/SMerz/papers/abz2016-pharos.html

The first category of problems deal with tooling. TLA+ doesn't have a great story when it comes to automation. There is no package manager. Version control is trickier than it needs to be (it's not obvious what files you might want to commit to git and which you shouldn't when you first start working with TLA+). There isn't a lot of support for automatically running things at the commandline (the community mostly uses the TLA+ toolbox, which is a GUI-based IDE). You can and people do these things, but they feel like distinctly second-class citizens. Really TLA+ feels tied to the TLA+ toolbox, warts and all.

The second problem is language support. TLA+'s main way of breaking down problems into modules and then using one module as an interface for another (its notion of refinement) suffers from problems analogous to the ones faced when dealing with inheritance. In TLA+'s case, it is easy to add additional new states into a state machine defined in another module (this is TLA+'s celebrated idea of stuttering), but is rather more annoying to do the opposite, e.g. show that in your new module a single state is meant to correspond to a two states in another module (e.g. you have a transaction primitive that allows you to assume that two states can be done simultaneously).

This is complicated by the fact that the easiest verification technique in TLA+ is model-checking, which fares the worst when dealing with transitive chains of logical implication. TLA+'s model checker does not have a native notion of logical implication. Instead the way you e.g. prove the statement A => B is by effectively proving A and B but privileging A to be the search space that the model checker operates in. This means chains of the form A => B, B => C, C => D and therefore A => D (and all the intermediate stages) are somewhat annoying. You either prove each step with separate models along the chain and just let a human infer that this means A => D, or you prove the statement A => (B and C and D), without using any of the intermediate implications.

Without robust support for transitive implication, the option of using composition in the traditional composition vs. inheritance debate becomes much less palatable as an option when it comes to inheritance.

To some extent this is a limitation inherent in model checking and goes away with the proof based verifier for TLA+ TLAPS. But there isn't a collection, that I know of, of proved theorems for TLAPS like many other theorem provers.

I suspect again this is due to both the lack of a package manager in the TLA+ ecosystem as well as some not so ergonomic parts of TLAPS. TLAPS feels very magical. Its main way of proving things is what's often referred to as sledgehammer or auto in other theorem provers; write the next step in your proof and hope the computer is smart enough to infer it from the previous step. It feels magical when it works. When the computer can't figure something out, it can be a huge pain to figure out why. It doesn't feel like I'm mechanically building up a proof so much as it feels like I'm playing a guessing game with the computer to see which leaps of logic it'll accept. This gets better with time as you develop an intuition of which leaps work and which don't, but can still be painful. This is mainly because TLAPS itself isn't a prover, but rather delegates to the "magic" methods of other provers.

Finally set theory and first order logic, the theoretical basis of TLA+, sometimes makes showing equivalence between items (which is vitally necessary when dealing with code written by multiple individuals who might use different encodings for the same idea) very difficult. In particular, trying to use the fact that A is equivalent to B, therefore some predicate P has an exactly analogous P' on B is tricky. Another way of stating this is that TLA+ as a language makes it a bit difficult to leverage isomorphisms and homomorphisms to reduce the amount of work you have to do. This is somewhere where alternative logical systems can have a big leg up.

All that being said, among the technologies commonly referred to as "formal verification," I would say that TLA+ is the one I would most commonly recommend to people in business situations. This precisely because of what many people view as a flaw, that TLA+ is a formal specification language and not a way to actually write or verify actual running code.

Because TLA+ specs are divorced from your codebase, they require far less buy-in to see dividends. You don't have to rewrite your codebase in another language. You don't even have to change your coding practices.

Indeed TLA+'s closest competitor on most teams is also precisely what most teams lack, which is high-quality documentation.

This means you can integrate TLA+ into your work with extremely little risk. Try formalizing your mental model in TLA+. See if it reveals interesting conclusions. If it does, congratulations! TLA+ has been useful to you and you can keep it around as an artifact detailing your thoughts in the future. If not, delete your specs and no harm no foul. No code depends on its existence. You don't need some lengthy transition period to migrate systems away from "using" TLA+. You lose no more time than the amount you put into writing your spec.

While we’re on the subject, I think it’s worthwhile to explain the name “formal methods”, and especially “formal” (methods just means techniques, in our case techniques for software verification), as I’ve seen people constantly misuse it.

Formal means mechanical, i.e. doable in principle by a computer (sometimes we say doable or checkable by a computer, but the two are equivalent from a computability perspective though not from a complexity perspective). So when you say you have a formal proof that does not mean you have a mathematical proof, but a proof that can be verified by a computer. Then why do we say "formal" instead of "mechanical"? Because the word formal was used for centuries before Alan Turing discovered that it is equivalent to "mechanical." The main idea of symbolic logic is that of the formula, or logical form; a sentence whose truth can be derived by the direct manipulation of its form (syntax) without any use of intuition or understanding. So, to this day, when we talk of things making use of symbolic (or formal) logic, we say formal rather than mechanical.

Now, if formal means mechanical and methods means techniques for software verification, are testing and type checking — both software verification techniques that are carried out by the computer — formal methods? Technically they are! But formal methods is also the name of an academic discipline, and so formal methods usually refers to whatever it is that people who research formal methods study, and type checking have not traditionally been a part of that discipline. What’s interesting that both of them — or, rather, certain forms of them — are now actually part of formal methods research. A few formal methods researchers study dependent type systems, type systems that can express a far richer set of program properties than simple type systems, and the study of concolic testing, a combination of symbolic and abstract interpretation/model-checking and concrete (i.e. “normal”) testing is a very hot topic in formal methods research at the moment. What's common to all topics in formal methods research is some use of formal logic.

BTW Paxos also has a leader - this is what makes these protocols efficient. They need only the linear number of messages instead of the quadratic "everybody talks to everybody" design.

I'd argue that the algorithm itself is simple, and that the difficult part is understanding why it works (i.e., why it satisfies the safety guarantees).

> It seems to be proof that trying to sound impressive is actually important.

I agree with this, and would add that making a paper sound impressive rarely conflicts with making it easy to understand. If anything, pointing out the contributions and applications of an approach help readers to understand that approach. At any rate, the same paper made easier to understand will generally be more likely to be accepted.