📌 一句话总结：波士顿 AI 代码翻译初创公司 Code Metal 完成 1.25 亿美元 B 轮融资，估值从 2.5 亿美元飙升至 12.5 亿美元，Salesforce Ventures 领投，客户包括美国空军、RTX（原雷神）和东芝，用「神经符号 AI + 形式化验证」解决 AI 生成代码的信任问题。
2026年2月21日 · 资讯分享 · 阅读时间约 5 分钟
三个月估值翻五倍，Code Metal 凭什么？
当整个行业都在讨论 AI 写代码有多快的时候，一家波士顿初创公司在问一个更尖锐的问题：AI 写的代码，你敢用在战斗机上吗？
Code Metal 给出的答案是：敢，但前提是每一行代码都经过数学级别的验证。
2 月 19 日，Code Metal 宣布完成 1.25 亿美元 B 轮融资，由 Salesforce Ventures 领投，Accel、B Capital、Smith Point Capital、J2 Ventures、Shield Capital 以及国防巨头 RTX（原雷神公司）跟投。公司估值从去年 11 月的 2.5 亿美元直接跳到 12.5 亿美元——三个月翻了五倍，正式跻身独角兽行列。
更值得注意的是，这距离他们的 A 轮（3600 万美元）仅仅过去了三个月。
不是又一个 Copilot，而是代码的「翻译官 + 公证人」
Code Metal 做的事情和 GitHub Copilot 完全不同。它的核心能力是跨语言代码翻译——把 Python、Julia、Matlab、C++ 等高级语言的代码，翻译成 Rust、VHDL 以及 Nvidia CUDA 等底层语言或硬件专用语言。
翻译本身不稀奇，市面上能做代码翻译的 AI 工具一大把。Code Metal 的杀手锏在于形式化验证（Formal Verification）：在翻译的每一步，系统都会生成测试套件，用数学方法穷举代码的所有可能状态，确保翻译后的代码与原始代码在功能上完全等价。
AI 可以以前所未有的速度生成代码，但在关键任务环境中，没有证明的速度是不够的——我们正在构建确保软件在部署前可被信任的基础设施。
— 来源：Code Metal CEO Peter Morales，SiliconANGLE
CEO Peter Morales 曾在微软和 MIT 林肯实验室工作，他表示 Code Metal 的可靠性测试符合 MC/DC 标准——这是航空飞控软件使用的验证标准。换句话说，如果翻译过程中出现无法验证的情况，系统会直接告诉你「这段代码无法完成翻译」，而不是悄悄塞给你一个带 bug 的版本。
客户名单说明一切
Code Metal 的早期客户阵容相当硬核：
| 客户 | 领域 | 应用场景 |
|---|---|---|
| 美国空军 | 国防 | 遗留系统代码现代化 |
| RTX（原雷神） | 国防/航空 | 关键任务代码翻译 |
| L3Harris | 国防电子 | 代码验证与迁移 |
| 东芝 | 工业电子 | 跨平台代码移植 |
| 博世 | 汽车/工业 | 嵌入式系统代码翻译 |
此外，Code Metal 还在与一家大型芯片公司洽谈跨芯片平台的代码可移植性合作（具体名称未披露）。
Karpathy 一条推文，说透了这个赛道
Code Metal 的 CEO 在接受 WIRED 采访时，直接引用了 Andrej Karpathy 最近的一条推文：
C 到 Rust 的移植势头越来越猛……我们很可能会把人类写过的大部分软件重写很多遍。
— 来源：Andrej Karpathy via WIRED
Morales 说：「他那条推文，就是我们在做的全部事情。」
这不是夸张。全球有数十亿行遗留代码运行在关键基础设施上——从卫星通信到电网控制，从飞行控制到工业机器人。这些代码大多用 C、Fortran、Ada 等老语言写成，维护它们的工程师正在退休，而新一代开发者对这些语言越来越陌生。
B Capital 合伙人 Yan-David Erlich 说得更直白：「控制通信基础设施甚至卫星的代码，很多都是老旧的、用人们不再使用的语言写的。它需要现代化。但在翻译过程中，你可能会引入 bug——这在关键系统中是灾难性的。」
AI 代码信任赛道正在成型
Code Metal 并不孤独。过去两年，一批围绕「AI 代码可信度」的初创公司密集获得融资：
- Antithesis — AI 代码自动化测试
- Code Rabbit — AI 代码审查
- Synthesized — 测试数据生成
- Theorem — 代码验证
- Harness — AI 代码安全
WIRED 将这些公司称为 AI 淘金热中的「卖铲子的人」——它们不直接生成代码，而是确保 AI 生成的代码值得信赖。当 AI 编码工具的产出量越来越大，验证和信任层的价值只会越来越高。
富贵点评
Code Metal 的故事揭示了 AI 编码赛道一个被严重低估的分支：不是谁写代码写得快，而是谁能证明代码是对的。当 Copilot 们在比拼生成速度的时候，Code Metal 在卖「数学级别的信任」——而且卖给的是最不能出错的客户：军方和航空航天。
三个月从 A 轮到 B 轮、估值翻五倍，这个速度本身就说明市场对「可验证 AI 代码」的需求有多饥渴。Karpathy 说得对，人类写过的软件迟早要被重写很多遍——但重写的前提是，新代码必须比旧代码更可靠，而不是更快但更危险。Code Metal 押对了这个逻辑。
📋 要点回顾
- 融资规模：1.25 亿美元 B 轮，Salesforce Ventures 领投，估值 12.5 亿美元（三个月前仅 2.5 亿）
- 核心技术：AI 跨语言代码翻译 + 形式化验证，每一步翻译都生成数学证明确保正确性
- 客户阵容：美国空军、RTX、L3Harris、东芝、博世等国防和工业巨头
- 行业背景：全球数十亿行遗留代码亟需现代化，AI 代码信任赛道正在快速成型
- 竞争格局：与 Copilot 类工具不同，Code Metal 专注「代码翻译 + 验证」的垂直场景，瞄准关键任务市场
❓ 常见问题
Q: Code Metal 和 GitHub Copilot 有什么区别？
A: Copilot 是「AI 帮你写新代码」，Code Metal 是「AI 帮你把已有代码从一种语言翻译成另一种语言，并用数学方法证明翻译是正确的」。两者解决的是完全不同的问题，Code Metal 更偏向关键任务场景。
Q: 形式化验证是什么？为什么重要？
A: 形式化验证是用数学方法穷举程序所有可能的运行状态，证明代码不存在特定类型的错误。传统测试只能覆盖有限场景，形式化验证理论上可以覆盖所有场景。在航空飞控、军事系统等不允许出错的领域，这是刚需。
Q: 为什么遗留代码翻译是一个大市场？
A: 全球关键基础设施中运行着数十亿行用 C、Fortran、Ada 等老语言写的代码，维护这些代码的工程师正在退休，新开发者不熟悉这些语言。同时，Rust 等内存安全语言的兴起让代码迁移变得更加迫切——美国政府已经明确建议关键系统迁移到内存安全语言。
作者：王富贵 | 发布时间：2026年2月21日
参考来源：WIRED · SiliconANGLE · TechFundingNews