一句话：回顾 Project Everest 近十年用程序验证构建工业级高保障安全通信软件的经验与得失。
本文回顾了微软研究院于2016年启动的 Project Everest。该项目与 INRIA 和卡内基梅隆大学合作，旨在推动程序验证研究以产出工业级软件，具体目标是为 HTTPS 生态中的安全通信软件提供可直接替换的经过验证的实现，涵盖 TLS、底层密码学及相关子协议。近十年后，作者从项目参与者的视角反思其成功与失败，总结工业级高保障软件在验证、工程化与部署中的经验，并展望未来十年程序验证研究的方向。文章并非提出新的验证技术，而是以经验报告和展望的形式，讨论形式化验证从学术原型走向实际生产系统所面临的挑战与机遇。
Project Everest began at Microsoft Research in 2016, aiming to spur research in program verification to produce industrial-grade software. In collaboration with INRIA and Carnegie Mellon University, Project Everest’s goal was to produce drop-in verified replacements of secure communications software used in the HTTPS ecosystem, including TLS, the underlying cryptography, and related subprotocols. Now, almost a decade later, we reflect on the project, sharing both its successes and failures, and look ahead to the next decade of program verification research.
@article{AhmanBBBBDFFGHHKMNPPRRR26,
title = {Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software},
author = {Danel Ahman and Karthikeyan Bhargavan and Barry Bond and Jay Bosamiya and Christopher Brzuska and Antoine Delignat-Lavaud and Cédric Fournet and Aymeric Fromherz and Sydney Gibson and Chris Hawblitzel and Cătălin Hrițcu and Markulf Kohlweiss and Guido Martínez and Haobin Ni and Bryan Parno and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Exequiel Rivas and Nikhil Swamy and Santiago Zanella-Béguelin},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {48},
number = {2},
year = {2026},
doi = {10.1145/3805702}
}