F* 官网这次更新的介绍页里，罗列了一份颇为亮眼的“生产采用”名单：Firefox、Linux 内核、Windows Hyper-V、WireGuard、Tezos、ElectionGuard，几乎覆盖了从浏览器到区块链的半个安全软件版图。乍看像是形式化验证终于杀进了产线。
但拆开看会发现，名单里被采用的往往是某个具体模块——一段 Curve25519 实现、一个报文解析器——而不是整套密码学子系统。搞清楚这个颗粒度，比记住这份名单本身更重要。
F* 是什么，名单里到底换了什么
F* 是微软研究院和 Inria 主导的“面向证明编程语言”，架构师是 Nikhil Swamy，团队里还有 Karthikeyan Bhargavan、Cédric Fournet、Jonathan Protzenko 等人。它用依赖类型描述程序性质，靠 SMT 求解器和交互式证明策略验证，代码默认编译到 OCaml，也能经 KaRaMeL 提取成 C、Wasm，或用 Vale 提取成汇编——终点是能跑的产品代码，不是纸面定理。这也是它跟 Coq、Isabelle 这类偏学术验证工具最大的分野。
真正落地的是 Project Everest 系的几个库：写密码学原语的 HACL、写验证汇编的 ValeCrypt、把两者拼起来的 EverCrypt，以及生成报文解析器的 EverParse。Firefox 和 Linux 内核采用的多是 HACL 里 Curve25519 一类具体原语；WireGuard 引用了同源代码；而 Windows 那边写进 Hyper-V 的其实是 EverParse 生成的报文解析器，用来在 Azure 网络层校验数据包格式，跟密码学原语是两码事。没有一个案例是把整套密码库或整个操作系统的安全子系统替换掉。
证明覆盖了什么，没覆盖什么
形式化验证这四个字容易被理解成绝对安全，但 F 的证明范围其实划得很窄。HACL/EverCrypt 的证明覆盖内存安全、功能正确性，以及部分实现的恒定时间行为——能挡住缓冲区溢出和某些侧信道计时攻击。它证明不了编译器有没有把代码翻译对、操作系统调度有没有出岔子、CPU 本身有没有微架构缺陷，更别说推测执行漏洞或硬件故障。
验证的是这段代码本身，不是它运行的整台机器
这个边界对工程师不是新闻，但对读到“Firefox 用了形式化验证密码学代码”这类说法的普通读者来说，很容易脑补出过度的安全感。
验证代码跑得动吗
性能是这类项目长期被质疑的地方——证明正确性会不会拖慢速度？Jonathan Protzenko 等人在 2020 年 IEEE S&P 上发表的 EverCrypt 论文给出过一次系统性的回答。
结论清楚：可移植的 HACL* C 代码和普通手写 C 代码性能相当；打开向量化和硬件加速路径之后，EverCrypt 能接近甚至持平主流密码库。论文也承认，在部分深度调优的架构特定场景下，OpenSSL 靠手写汇编仍然更快。
- 结论.验证代码已经能跑，只是还没在所有场景都追上手写优化库
谁在维护它，接下来看什么
F* 没有一份对外发布的 2025—2026 正式路线图，实际进展分散在 GitHub 的 milestone、issue 和历次 release notes 里，靠 Nikhil Swamy 这批核心贡献者和社区协作推进。这种松散但持续的节奏，短期内不会变成某家公司的重点产品，更像学术团队和工程团队的长期磨合。
对使用 Firefox、WireGuard 或考虑接入 HACL/EverCrypt 的工程团队来说，现实的判断是：可以放心复用具体的、经过验证的原语，但不能把“接入了 F 生态”等同于“整条安全链路都被证明过”。接下来值得盯的，是 F* 团队会不会补一份正式路线图，以及 EverCrypt 会不会在更多硬件平台上追平 OpenSSL 的调优优势。
- 风险.把“选定原语已验证”误读成“整套系统已验证”，是这类新闻最容易踩的坑