如何自举可验证软件栈：以 nixpkgs 为蓝本估算全量形式化验证成本

文章以 nixpkgs 的依赖链为蓝本，估算对全部软件做形式化验证的成本与时间：若模型验证能力每两个月翻倍，每年投入 1 亿美元可在 2027 年底前验证 95% 的机器码，总成本约 1.34 亿美元。