You can easily convince me that formal methods are more efficient for complex distributed systems problems, or for cryptographic protocols, or things like that. But even in systems whose whole premise is algorithmic, the hairy stuff provers are designed against are a small part of the overall coding task.

And for the kind of security this article is talking about, it's not enough to have a proven core algorithm or protocol; your dumb input parsers and output renderers and all that other boring integration code also needs to be bug-free, because those kinds of joinery are where we tend to find vulnerabilities.

Indeed. What is unbearably slow is creating the whole software with formal verification, not just the core algorithm.

TLA+ doesn't prove anything to be "correct" or "flawless", I find it extremely worrisome that you claim as much. It failed to exhibit traces that violated your invariants, which says something completely different.

1. TLA+ doesn't "find" or not find anything. It is a mathematical language for describing systems and assertions about them. There is a proof assistant for TLA+ that checks your formal proofs of theorems that say that your assertions follow from the description, and model checkers that verify your theorems automatically.

2. If you use the model checker, it's not about it "failing to find" a counter example. A model checker result is a proof that no such example exists. True, it is usually a proof about some finite instance of your system description.

3. There is just no such thing as proving a system flawless. Software systems are physical systems exhibiting probabilistic behaviors. At best you can prove things about a mathematical description of a system, which mean that as long as the physical system behaves according to the description, the result follows. Of course, the first part at best holds with some probability.

I've never actually used TLA+, but my understanding is that it does exhaustive model checking (presumably using some suitable simulation relation), so in this case failure to find a violating trace indicates that no such trace exists, and the invariants always hold.

Correctness might well be defined solely by a set of invariants, so I don't quite understand your point here?

Imagine the following scenario, you have encountered an actual bug in concurrent code, and you think it would be great to work on a model and invariants that lets TLA+ find the bug (as an exercise).

So you start writing a model, and a set of invariants, you run the tool and... it finds nothing. Does that mean you just proved the bug does not exist? No, you _know_ the bug exists, what it means is that you didn't write a correct model on your first try. So you iterate on it, add a few things you missed, put some extra labels, read the docs a bit more, maybe refine your invariants, make them stronger, work through a couple traces that don't actually make sense in practice (e.g. actors just never taking any action whatsoever). During all this time, you either found nothing or things that were not interesting. At no time have you ever proved anything correct, you just iterated on your model until you managed to capture a real life scenario.

It takes some convincing to make the jump from "this model does not violate my invariants" to "I think this model and the invariants are close enough to what I care about that I think it's good enough"... I don't know how to go from there to things like "proven correct" and "flawless".

I mean, specific to my scenario, my invariant was "only one zone at a time" and the liveness property was "everyone who wants a zone eventually gets one", so respectively:

1. \A z \in Zones: Active(z) => ~\E o \in Zones: z # o /\ Active(o) 2. \A w \in Workers: \A z \in Zones: WorkerWantsZone(w, z) ~> WorkerHasZone(w, z)

Unlike your scenario, I am checking the spec here. I know that code that properly implements the spec satisfies these two properties, therefore I've proven the spec correct. You can disagree on the importance of those two properties but I've mechanically checked that those properties are always preserved in my finite models, so I know the spec is correct, at least for the model size.

You know, it's really not too hard to get started with this stuff. You can always nit-pick but why not try it out and see if it's useful for you?

I am using it, I just don't use it to make claims of correctness.

Ah sure. I interpreted "proven correct" to mean "proven correct wrt a set of invariants" in this context.

This is correct: the TLA+ model checker (TLC) will check all possible behaviors for the finite model. As the GP said, they were only working with a finite number of workers, but within those constraints it guarantees the spec always satisfies the invariants.

(This is of course assuming that TLC doesn't have any bugs that would cause it to misreport. By contrast something like randomized testing doesn't guarantee the spec satisfies the invariants even if the tester is bug-free.)

exactly. I've proven that in a scenario with a certain number of zones and workers, the invariants and temporal properties cannot be violated.

With more work, I could prove the invariants for any number of workers and zones using TLAPS rather than TLC, though I couldn't prove the temporal properties in this way (since TLAPS doesn't support temporal logic, it can only prove invariants.)