A clarification:
> Instead of writing proofs, it works using the simple method of running all possible executions of a program.
TLA+ is a formal mathematical language designed to describe digital (and hybrid digital-analog) systems. By itself it "does" nothing other than allow writing a formal description of a system, various propositions about it, and their proofs.
There are tools, however, for mechanically writing and checking TLA+ proofs with a proof assistant (TLAPS), as well as model-checking them (TLC). The author refers to the latter, but it should be noted that model checkers, including an explicit-state model checker like TLC, don't only not run all possible executions of a program, they don't even run it once. They are "static." Indeed, TLC could, in some situations, check whether an uncountably infinite number of program executions, each of which of infinite length, satisfy some proposition within seconds.
Also, the author chose to specify their algorithm in PlusCal, rather than in TLA+, which is pseudocode-like a language that compiles to TLA+ in a straightforward manner and is sometimes more convenient than TLA+ to specify low-level concurrent algorithms (TLA+ is more convenient to specify a higher level view of an entire system).
TLA+ is, however, exceptionally pragmatic due to an availability of a model checker for it (in fact, there are now two model checkers for TLA+, TLC and Apalache, using very different algorithm), but mostly because it is exceptionally easy to learn compared to other formal mathematical languages.
This is something I never quite understood with TLA+ (just from reading articles here and there, never actually used it).
Let’s say I have a piece of C++ code and a TLA+ model for what it should be doing. How do I validate the C++ code with it?
A better question to ask is how do I formally derive a program that satisfies a given specification? Then validation is just mathematical “checking your work” and is easy or even trivial.
Except that's another question to which the answer is currently, "you don't", at least not at any interesting scale, not with TLA+ and not with anything else. But TLA+ is a tool aimed to help achieve correctness effectively, i.e. get a good cost/benefit for it. Between the highly scalable, low-confidence, testing, and the high-confidence, low-scale end-to-end verification, there's a huge swath of software correctness techniques, and the flexible TLA+ tries to hit a rather large swathe of that spectrum.
In other words, we ask, is this better than what we do now in a sufficiently large portion of cases, rather than is this the silver bullet? The answer to the second question is no. I think the answer to the first one is yes.
Formal program derivation satisfying a given specification has been around for well over half a century now. Hoare logic and the predicate calculus are entirely adequate for formal derivation in any language with well-documented semantics. Lamport himself has contributed significantly to the field. Unfortunately the American dominated programming industry has a strange phobia about mathematical reasoning[1]. The irrationality is exposed by patently ridiculous statements like that formal derivation doesn't scale. If you believe that, then you can't believe any nontrivial results from the hard physical sciences or pure mathematics. The actuality is that formal derivation makes building nontrivial constructs considerably easier. It is a tool, and like any tool when used properly it acts as a capability multiplier.
[1] This is doubly confusing to me because it's not a matter of difficulty. Anyone with the mental horsepower to learn a modern programming language is easily capable of gaining proficiency in the predicate calculus.
That's like saying that we've been able to turn lead into gold for a while now. It depends on what you mean by "we" and by "can." Some specialists have turned some lead atoms into gold in a billion-dollar particle accelerator.
Common, "ordinary" software can neither be mechanically derived nor verified using any feasibly affordable process at common scales. Let me remind people that the largest programs ever verified end-to-end were one-fifth the size of jQuery, and they required world-experts years of effort as well as careful simplification.
I've written a fair bit on program correctness and formal verification/synthesis [1], and I, myself, am a practitioner and advocate of formal methods, but I am not aware of any in-the-field, industrial scale, general (non-niche), non-specialist, repeatable, affordable formal synthesis/verification techniques that can handle systems and specifications of the scale TLA+ is commonly used for by ordinary engineers. If you know of such examples, I'd be interested in seeing them.
“P is a language for asynchronous event-driven programming. P allows the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events. P unifies modeling and programming into one activity for the programmer. Not only can a P program be compiled into executable code, but it can also be systematically tested using Model Checking. P has been used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone. P is currently being used extensively inside Amazon (AWS) for model checking complex distributed systems.”