4 ms·
My understanding is that TLA+ is primarily used for model checking not correctness proofs. I've dug around for TLA+ proofs and found only simple examples. That
by uluyol 8y ago
My understanding is that TLA+ is primarily used for model checking not correctness proofs. I've dug around for TLA+ proofs and found only simple examples.
That being said, model checking alone is really powerful and can uncover serious design flaws.
- pron 8y agoYou can find some big deductive proofs here: https://members.loria.fr/SMerz/papers.html https://members.loria.fr/SMerz/papers.html But you're right that deductive proofs are hardly ever worth the effort when you have a model checker. If you can get 99.99999% confidence for essentially free, most people wouldn't pay extra months of work to get to 99.999999% confidence.