OpenAI 老兵推 Code Contracts:用非形式化契约做 agent 代码验证
TacoCohen · x · 2026-09-11
曾在 OpenAI 从事多年形式化方法工作的 spolu 认为:虽然自动定理证明如今已免费,但我们不会对所有代码做完整形式化验证——现实太混乱,代码仍是工程手艺的核心,因为只有能维护才算真正理解系统。他认为完全非形式化与完全形式化验证之间存在一个高效边界,并发布了开源格式 Code Contracts 来探索这条边界。
核心思路是「验证——但非形式化,而是 agentic」:
- 结构化契约与代码同置:用 @cc 指令在代码旁以自由文本写出不变量、规格与编码规则(如余额不足时支付必须失败且不改变余额),格式小到可以放在注释里;
- 元数据支持发现与提醒:owner/notify/label 等字段让系统能为某行代码找到所有相关契约,并在检测到重要违规时持续验证、发出通知;
- 解决两个痛点:同置防止规格随时间漂移;显式契约让稀缺的代码评审注意力更省力,也给 agent 提供明确的假设与验证信号,帮助其发现错误、改进实现。
这为 agent 驱动的软件开发提供了一种介于 PDD(纯提示驱动)与全形式化验证之间的务实中间路线。
「漫话AGI」频道最新
- Timnit Gebru 批 AI 末日论:意在分散对自主武器等真实危害的注意力 — nordicinst · 2026-09-11
- 质疑OpenAI对智能体安全事件零披露：10个被攻击网站、德国wiki均未公开 — Hesamation · 2026-09-11
- 读者呼吁书店标注AI写作比例：我不想读AI生成的散文 — Philmod · 2026-09-11
- 回声两种观点：看不懂指数增长是人类对 AI 最大误判 — GregCook2011 · 2026-09-11
- 程序员对比：AI 冲击创意行业遭抗议，软件工程师却"平静接受" — basedjensen · 2026-09-11
- 新论文：自复制程序靠合作进化涌现，博弈论统一计算起源 — AdaptiveAgents · 2026-09-11