News for hackers. Stuff that matters.

A comment on Introduction to TLA+ Model Checking in the Command Line. Parent comment

Re:Introduction to TLA+ Model Checking in the Command Line by uluyol on Friday January 18, 2019 @03:05AM (#18937745)
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.

[ Parent | on HN ]
Re:Introduction to TLA+ Model Checking in the Command Line by pron on Friday January 18, 2019 @07:09AM (#18938725)
You can find some big deductive proofs here: 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.

[ Parent | on HN ]