I misread the title as "proof work" not "proof _of_ work." The analysis makes sense, but has kinda always been true. So mostly depressing rather than insightful.

But part of me has been wondering for a while now whether proofs of correctness is the way out of the NVIDIA infinite money glitch. IDK if we're there yet but it's pretty much the only option I can imagine.

Every formal verification depends highly on requirements. It's pretty easy to make a mistake in defining the task itself. In the end, you'd want to verify system behavior in real world, and it's impossible to completely define real world. You always make some assumptions/models to reason within, and it impossible to verify the assumptions are correct.

I think there's definitely more scope for ruling out vulnerabilities by implementing simpler designs and architectures.

good luck formally verifying everything