First, the art and science of formal verification has largely moved away from proving programs correct to better/cheaper ways of catching more bugs (at least when mainstream software is concerned). So the most important question is "is a TLA+ specification a cost-effective way of catching bugs even without a formal tie to the implementation?" My opinion on that is an emphatic yes. (BTW, code reviews are an effective assurance technique even though they're not formal at all).
However, there are ways to create formal ties between a TLA+ spec and a running program. As always, the sounder the method the more costly it is (and the cost often grows faster than the increased confidence). One approach that is being research is checking execution logs against the model, perhaps online as the program is running.
At the end of this talk, https://youtu.be/TP3SY0EUV2A, I mention the technique and theory behind it, referring to this paper, Model-Based Trace-Checking [1]. I believe research is ongoing and you can find more recent papers on the subject.
I have no idea how well it works, but it seems pretty interesting.
I do think that that's something a bit more compelling about something like Isabelle, which offers first-class support for exporting programs that can be directly executed, which in theory would inherit all the proofs for the parent Isabelle (though that's not strictly true).
But this exact problem is why I am more interested in approaches that integrate specification and implementation into a single (dialectical) process (e.g., via type-theoretic methods).
Someone writes theorems, prove them in their head, and try to write down that proof.
Someone else reads both and tries to reason about the proof and theorem and notifies the creator of there are mismatches.
A more practical person goes and translates all that math/theory to code.
Another practical person will check implementation and theory and notify the implementor of mismatches.
TLA+ is basically an automated version of step two in this process. Someone has an idea for a theorem, writes it down in TLA+ and the system will notifyil if it makes any sense.
Welcome to the research field of program refinement. There are a couple of approaches one can take:
- Certify: the program isn't actually checked/proven to satisfy the spec, but experts in the field will pore over the code and try to find any disparities or edge cases.
- Top-down: given a spec, try to generate an implementation that satisfies it by construction. This depends a lot of the concrete framework, but e.g. Coq supports extraction of executable code from its (verified) source. The results are not very well decoupled from the spec and are often lacking in performance (single-threaded, unoptimised, etc).
- Bottom-up: given an actual implementation, prove that it behaves according to the spec. This can allow for optimised programs and concurrency, but both complicate the proofs. (This happens to be my PhD research topic.)
Some work to look at, if you are curious: Event-B, Trillium, IronFleet
How do I can check an implementation against a TLA+ spec?
First, the art and science of formal verification has largely moved away from proving programs correct to better/cheaper ways of catching more bugs (at least when mainstream software is concerned). So the most important question is "is a TLA+ specification a cost-effective way of catching bugs even without a formal tie to the implementation?" My opinion on that is an emphatic yes. (BTW, code reviews are an effective assurance technique even though they're not formal at all).
However, there are ways to create formal ties between a TLA+ spec and a running program. As always, the sounder the method the more costly it is (and the cost often grows faster than the increased confidence). One approach that is being research is checking execution logs against the model, perhaps online as the program is running.
At the end of this talk, https://youtu.be/TP3SY0EUV2A, I mention the technique and theory behind it, referring to this paper, Model-Based Trace-Checking [1]. I believe research is ongoing and you can find more recent papers on the subject.
[1]: https://arxiv.org/abs/1111.2825
I haven't tried it yet, but there is a PlusCal-to-Go compiler now: https://distcompiler.github.io/
I have no idea how well it works, but it seems pretty interesting.
I do think that that's something a bit more compelling about something like Isabelle, which offers first-class support for exporting programs that can be directly executed, which in theory would inherit all the proofs for the parent Isabelle (though that's not strictly true).
You can do [model based testing](https://en.wikipedia.org/wiki/Model-based_testing) (e.g., https://mbt.informal.systems/)
But this exact problem is why I am more interested in approaches that integrate specification and implementation into a single (dialectical) process (e.g., via type-theoretic methods).
Someone writes theorems, prove them in their head, and try to write down that proof.
Someone else reads both and tries to reason about the proof and theorem and notifies the creator of there are mismatches.
A more practical person goes and translates all that math/theory to code.
Another practical person will check implementation and theory and notify the implementor of mismatches.
TLA+ is basically an automated version of step two in this process. Someone has an idea for a theorem, writes it down in TLA+ and the system will notifyil if it makes any sense.
Welcome to the research field of program refinement. There are a couple of approaches one can take: - Certify: the program isn't actually checked/proven to satisfy the spec, but experts in the field will pore over the code and try to find any disparities or edge cases. - Top-down: given a spec, try to generate an implementation that satisfies it by construction. This depends a lot of the concrete framework, but e.g. Coq supports extraction of executable code from its (verified) source. The results are not very well decoupled from the spec and are often lacking in performance (single-threaded, unoptimised, etc). - Bottom-up: given an actual implementation, prove that it behaves according to the spec. This can allow for optimised programs and concurrency, but both complicate the proofs. (This happens to be my PhD research topic.)
Some work to look at, if you are curious: Event-B, Trillium, IronFleet