The bet that complex proof systems have no bugs that would let someone prove something false.
Why it matters: Matters more and more as Ethereum plans to rely on proofs instead of re-running blocks.
On the map: zkVM circuits and provers, formal verification in progress, k-of-n proofs tolerate one bad prover
Zero-knowledge virtual machines are large, complex systems, and soundness bugs (a prover convincing a verifier of something false) have been found in production provers[1].
Plans that let Ethereum validators rely on execution proofs assume the proof systems are sound and correctly implemented. Today's ZK rollups and privacy apps already rely on the same kind of bet for their own circuits (the "ZK circuits" box in the live section). Requiring proofs from several independent systems (for example 2 of 3)[2] tolerates a bug in one. Formal verification of leanVM and zkEVMs is underway[1].
If any of these breaks, this breaks too.
If this breaks, these break with it.