Cryptographic protocols hold up the digital world, and almost nobody gets them right — the adversary never follows the rules — so the case that breaks you is the one you never imagined. You've got three options:
The problem with these traditional techniques is disconnection from reality. State of the art:
We're some way from proven executables, and we aren't throwing away the internet; one way to combat inevitable vulnerabilities is autonomous elimination (cybernuke'26), others stop erroneous code:
Applied pi calculus turns a protocol into manually verifiable process (IOS'11); ProVerif reasons automatically (manual'23). Guarantees mattering most: Indistinguishability of worlds; runs differing only in cryptographic material look identical. Stakeholder vote indistinguishable from any other with same collective score, individual preferences hidden. Authentication, confidentiality, privacy — all observational equivalences, which ProVerif's shortcut collapses for. Fixing that was part of my PhD'11; barrier synchronisation landed in ProVerif 1.94 (JCS'18).
Unwinnable games are the study of cryptography. Security is framed as breakout: Can adversary craft execution causing disarray? Absence of such an adversary implies easy life. Hopping game to game, we prove by reduction — protocol is secure assuming foundations are — free & fair governance constructed from non-malleable encryption (IWSEC'15) and zero-knowledge proofs (Fiat-Shamir'25), that reduces to (is-secure-if) cryptographic primitives are secure (JCS'21). Gateway to proven executables is gaming.
Agents are writing proven executables: We just install cryptographic games in theorem provers, they reason over source code to prove security of equivalent executable. Formulating games remains gruelling; the game is the security definition: You pin down what the adversary may do, and what's a break. Too strong, nothing's provable; too weak, you prove the wrong thing. History teaches we're more wrong than right.
When something is said to be proved (election legitimacy, say) above techniques guarantee protection.
A proof persuades, and persuasion is the flaw — the literature is full of arguments that convinced everyone and broke years later. A theorem prover persuades no one; it checks, every step, every case, granting nothing to intuition or authority. So, when we say proven executable, we don't mean a case was made; we mean a machine exhaustively searched, finding no way to disagree. But that search only covers the game we hand it. Games are the linchpin: Formulating them, not checking them, is where the challenge lies.