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, what's a break, too strong, nothing's provable; too weak, the wrong thing. History teaches we're more wrong than right.
When something is said to be proved, e.g., election legitimacy, 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.