And so aphyr gets paid, for instance.
You may not even be able realistically to run a test case. The laws of life say your 10000 core compute job will fail non-deterministically only after a day or so. It would clearly be helpful to have at least some formal guarantees, such as liveness at some level.
Complicated proofs I do not understand, without much effort.
And I surely know that you can make mistakes with test cases as well. So I surely do not claim my way to be superior. But it works way better for me.