Test cases are not necessarily simple to understand.
Especially the test cases needed to trigger some deep bug.
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.