Forrmal methods have a long history as both an exciting topic and one that seems perennially to avoid living up to its hype. However, I’ll make the case that things have gotten serious lately, in what I like to summarize as mechanized, end-to-end proofs of functional correctness. I think they’re going to be big in the next few years, and I’ll try to give a preview of how. Most of the talk will be about our recent, successful experiment in using the Coq proof assistant to generate intricate cryptographic code automatically, achieving good performance at the same time as we get first-principles proofs of correctness. Our generated code now powers (in a small but important role) about half of all HTTPS connections from browsers worldwide, via adoption in Chrome. I’ll finish the talk with some speculation about opportunities to redesign our computing stacks when we can commit to applying mechanized proofs throughout.