Comment on Reproducing the AWS Outage Race Condition with a Model CheckerparentComments−pjmlp10moWe have all seen how well it gets surfaced automatically at AWS.−zozbot23410moThere might be plenty of potential failures that we haven't all seen, simply because the problems were fixed after TLA+ modeling brought them up.−pjmlp10moOr it might be that the model doesn't really avoid all possible human failures when translating TLA+ into Java, C++ metatemplate programming, or whatver.
Comments
We have all seen how well it gets surfaced automatically at AWS.
There might be plenty of potential failures that we haven't all seen, simply because the problems were fixed after TLA+ modeling brought them up.
Or it might be that the model doesn't really avoid all possible human failures when translating TLA+ into Java, C++ metatemplate programming, or whatver.