(I'm the author of the original post.) Model-checkers don’t prove that a program is correct, only that the logic in the program’s abstracted and simplified comm

(I'm the author of the original post.) Model-checkers don’t prove that a program is correct, only that the logic in the program’s abstracted and simplified communications/state model has no inherent race conditions, deadlocks and so forth, i.e. no typical concurrency flaws. Model-checkers don’t “prove” correctness in the mathematical sense (and maybe I should have written “verifiably-correct” instead of “provably-correct”). Rather, model-checkers search for counterexamples to the hypothesis “there are no concurrency flaws in this model”, by exhaustively tracing through all possible distinct execution paths through the model. Amazon calls their models “exhaustively testable pseudo-code”. If no counterexample is found, then we can be sure the model has none of the standard concurrency flaws, and we can be sure that the communications “housekeeping” code auto-generated from the model will have none either. This is a limited yet extremely powerful and valuable aspect of correctness, the hardest kind of correctness for humans to achieve in concurrent software. I believe software engineers can and should start routinely using model-checking on concurrent logic, taking advantage of the machine’s ability to race relentlessly through enormous numbers of execution paths to uncover subtle flaws in logic. Even a small change to concurrent logic can have far-reaching consequences that are very hard for humans to envision. I believe competitiveness and sound engineering practice demand use of model-checkers on concurrent logic.