This article is a companion piece to What Works (and Doesn't) Selling Formal Methods. It began life as part of a talk I gave in late 2024. Some things are difficult, and some things are merely expensive. Imagine this: aliens are coming to kill us all. Humanity sends its best negotiators, and the aliens announce that they will call off their horrible assault only if we release a formally verified version of GCC, every damn line of code… in ONE YEAR. After some understandable confusion, the heads of the G7 summon Xavier Leroy, hand him an enormous check, and tell him to get on with it. Pretty soon, warehouses of mathematicians around the world are proving Rocq theorems day and night. The coordination challenges are enormous, but they get it done! The aliens go home, Xavier wins a Fields medal, EGOT, and all five Nobel prizes,1 and everyone else goes back to worrying about AI. The point I’m making is that we basically know how to build a formally verified compiler—we already did it. The same is true for formally verified cryptographic libraries, parsers, and microkernels. The reason that GCC hasn’t been formally verified is that to do so would be absurdly expensive. It wouldn’t be beneficial enough to justify the cost. But if aliens do show up, I bet we could do it for less than the cost of MCU Phase 3 ($2.2–2.4 billion). Okay different story: aliens are coming to kill us all and they demand a formally verified web browser. Xavier sticks his hand up (they brought him t