Tests are simple to unterstand.
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.
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.
How is this any different? You can still make mistakes in your test code, test data, omit cases that would fail, etc. I think I'd be less confident in a set of unit tests than I would with an automated proof checker.