自动驾驶行业有一张默认的成绩单：里程。谁跑得里程多，谁就“更安全”。各家企业定期公布测试里程数据，像在交一张越来越长的答卷，但很少有人问一个尖锐的问题：跑得里程多，就能证明一辆无人车更安全吗？

RAND的研究曾做过估算：要证明完全自动驾驶死亡率比人类驾驶低20%，大约需要88亿英里测试里程。这个经常被行业引用的数字，不是在提醒路测无用，而是在说：路测的证明力，比行业以为的要弱。它能增加信心，却很难穷尽所有长尾。

车能跑，不等于安全已被证明。

正是在这个行业共识的盲区里，曹操出行的动向引发关注：6月28日，曹操出行发布公告称，邀请图灵奖得主约瑟夫·希发基思（Joseph Sifakis）出任AI创新中心首席科学顾问，为RoboX战略提供可信自主系统领域的学术支持。

Robotaxi的安全逻辑要更新了。

一个图灵奖得主，追了一辈子的问题

Sifakis的研究，从半个世纪前一个朴素的问题出发：机器越来越复杂，人怎么知道它是可靠的？

1970年代，他从Petri网起步，描述并发系统的数学工具，多个进程同时运行互相依赖，如何判断系统不会陷入死锁、不会丢掉关键状态？人靠眼睛看不过来，靠测试跑不完所有路径。

这个困境促使他在1980年代转向模型检测，并与Edmund Clarke、E. Allen Emerson几乎同期独立发展了这一理论。通俗地说就是：用算法自动穷举一个系统所有可能的状态，检查有没有任何一个违反预设的安全属性。

测试只能发现错误，不能证明“没有错误”。而模型检测可以在给定模型下，证明系统不会违反这些属性。这套方法最终被Intel、IBM、微软等公司用于芯片设计、嵌入式软件、通信协议的日常生产实践，Sifakis也因此获得2007年图灵奖。

此后他的研究继续推进：模型检测擅长有限状态系统，但自主系统面对的是开放、动态、充满不确定性的世界。为此他主导开发了BIP框架（Behavior-Interaction-Priority），把复杂系统拆解为“行为-交互-优先级”三层抽象，每一层都可形式化验证，组合后整体仍是可证明安全的。他将这个思路概括为Safe-by-Construction：安全不是事后检测出来的，是在构造系统的时候就种进去的。

这和行业主流的“测试-迭代”逻辑形成鲜明对照：后者相当于“先盖起来用着，哪里裂了就补哪里”；前者相当于在画图纸的阶段，就用数学证明这栋楼在所有受力条件下都不会倒塌。

他追了一辈子的那个问题“机器凭什么值得信任”，伴随其加盟曹操出行，指向了Robotaxi。

安全的悖论：“跑里程”的证明力有边界

自动驾驶行业“谁跑的里程多谁就更安全”的默认共识，其实远比想象中脆弱。

因为路测回答的是“系统已经经历了什么”，形式化验证回答的是“系统理论上不会做什么”。前者是经验，后者是证明。经验可以让你放心，但证明才能让你确信。

监管也在往这个方向推进。美国NHTSA近年要求企业报告涉及自动驾驶系统的特定事故，安全正从企业自己的成绩单走向更透明、更可追踪的公共账本。问题是：谁来给这本账本写证明，而不是只写记录？

Sifakis的研究正好提供了一种不同的回答。对曹操出行而言，他的方法论不是停留在理论层面，而是对应RoboX战略的多个关键环节：Robotaxi控制器设计中，Safe-by-Construction将危险行为提前排除，为安全认证提供可验证依据；混合车队运营中，BIP框架帮助验证调度系统的正确性，降低异构系统协同风险；车-路-云协同场景中，CPS形式化设计提升整体系统运行可靠性。

更稳妥的路径不是抛弃路测和数据，而是让道路数据、仿真测试和形式化验证形成闭环。我的观点是：下一阶段的竞争，不是谁跑得更远，而是谁能把安全、成本和运营稳定性一起算清楚。单靠数据规模讲故事的阶段正在过去。

为什么是曹操出行？安全从"单车问题"变成了"系统问题"

AI正在从信息处理工具变成物理世界的决策与执行主体。大模型答错了可以重问，但一辆时速80公里的无人驾驶汽车做出错误判断，没有重试机会。物理AI进入现实世界，首先要回答的就是Sifakis追了一辈子的那个问题：它凭什么值得被信任？

6月18日，曹操出行宣布启动全面AI转型并发布RoboX战略：围绕智能定制车辆、智能驾驶技术、智能运营三大核心要素，构建覆盖Robotaxi、Robovan等场景的智能运力体系。2025年服务覆盖195个城市，月活用户4130万，全年营收202亿元（同比+37.7%）；2026年4月成为杭州首家获批进行Robotaxi无人化道路测试的企业；2030年目标部署10万辆Robotaxi与10万辆Robovan。

当车队规模从100辆到10万辆，安全就从单车问题变成了系统问题。

一个调度冲突、一次状态锁死、一条异常流程没有被及时收敛，都可能影响城市级运营稳定性。试点阶段可以靠项目经验兜底，跨城市、跨车型、跨业务的长期扩张，靠的是模型、规则和流程的复用能力，这恰恰是形式化验证最擅长的领域：一个被证明安全的调度规则，不需要在每个新城市重新"跑一遍"来验证。

这也是Sifakis出任首席科学顾问的核心使命所在：不是写论文，而是前瞻性确立系统边界，明确哪些行为必须受限、哪些流程必须验证、哪些异常状态必须预设安全冗余，哪些经验能在车队扩张中高效复用。Robotaxi的安全边界已经不只是行驶决策安全，而是贯穿定制车辆、自动驾驶、远程协助、智能调度、自动维保的全生命周期，每一个环节都需要能够验证、追溯、复用的安全机制。

哲学家维特根斯坦说过：“怀疑的终点不是不确定，而是对确定性的渴望。”自动驾驶行业跑了几十亿英里，恰恰说明：里程越多，对确定性证明的渴望越强。Sifakis加盟曹操出行，不是在否定路测的价值，而是在补上路测无法填补的那一环：从“相信它安全”到“证明它安全”。

后记：物理AI时代的信任证明题

曹操出行与Sifakis的合作，给行业带来的启示可能比这次任命更有价值：

第一，安全不能只靠事后验证，必须靠事前构造。测试-迭代模式在软件行业行得通，因为软件崩溃的代价是重启；但在物理AI世界，错误判断的代价是不可逆的。Safe-by-Construction不是替代测试，而是给测试划定可验证的边界。

第二，规模化部署的安全，需要可复用的证明而非可积累的经验。从100辆到10万辆，不能再靠逐个城市、逐辆车跑一遍来积累信心。形式化验证的最大优势是：一旦某个行为规则被证明安全，这个证明就是可迁移、可复用的，不需要在每个新场景重新验证。

第三，物理AI时代的信任，需要一本监管、保险和用户都能读懂的“安全账本”。 Robotaxi真正进入城市的那一天，行业要交出的不只是测试里程表，还有一套可审计、可追溯、可理解的安全证据体系。

Sifakis追了一辈子的那个问题“机器凭什么值得信任”，在物理AI时代变得更加紧迫，也更加现实。大模型答错了可以重来，自动驾驶没有这个奢侈。信任，在信息世界是态度问题；在物理世界，是生死问题。

在物理AI时代，这是所有想把自主系统送上真实世界的公司，迟早要面对的那道证明题。曹操出行请来一个图灵奖得主，不是为了多跑几英里，而是为了用一种新的方式证明安全。