研究测算：全面验证 nixpkgs 软件栈需上亿美元

Theorem 团队发布《Bootstrapping the Verified Software Stack》研究，以 nixpkgs 引导依赖链为蓝本，对全量软件做形式化验证的成本与路径进行建模：涉及 28,650 个包、154 GB 机器码。测算显示验证 95% 的机器码约需 1.34 亿美元、可在 2027 年底达成，而验证全部软件则约需 4 亿美元和 5 年时间。

2026-09-30 ~ 2026-10-01 · 2 条相关

• 建模 nixpkgs 全量形式化验证：95% 机器码或花 1.34 亿美元、2027 年底达成 — ctjlewis · 2026-09-30
• 研究测算：验证全部 nixpkgs 软件约需 4 亿美元、5 年 — ChrSzegedy · 2026-10-01