Most of cybersecurity at today's typical large corporation is reactive: we accept that the computer systems we deploy will be riddled with security vulnerabilities, so we focus on rapid response as individual issues are discovered. It's a cutthroat arms race against bad actors, who work to find new vulnerabilities as quickly as we can patch them. The venerable idea of formal verification offers a more principled solution: if we can build our systems alongside mathematical proofs of security, then we get out of the business of being surprised by specific vulnerabilities. The 21st century has actually seen very good progress on real-world realization of this idea, and I will give some examples from my work at MIT CSAIL, including our Fiat Cryptography project, which is used by all major web browsers to provide proved-correct code for cryptographic arithmetic. I will also explain the bigger-picture promise and remaining challenges of related technology.