That'll work great for your Distributed QSort Incorporated startup, where the only product is a sorting algorithm. Formal software verification is very useful.

That'll work great for your Distributed QSort Incorporated startup, where the only product is a sorting algorithm. Formal software verification is very useful. But what can be usefully formalized is rather limited, and what can be formalized correctly in practice is even more limited. That means you need to restrict your scope to something sane and useful. As a result, in the real world running thousands of tests is practically useful. (Well, it depends on what those tests are; it's easy to write 1000s of tests that either test the same thing, or only test the things that will pass and not the things that would fail.) They are especially useful if running in a mode where the unexpected happens often, as it sounds like this system can do. (It's reminiscent of rr's chaos mode -- https://rr-project.org/ https://rr-project.org/ linking to https://robert.ocallahan.org/2016/02/introducing-rr-chaos-mode.html https://robert.ocallahan.org/2016/02/introducing-rr-chaos-mo... )