用 AI 形式化验证系统 Aristotle 证明 OpenTitan 根信任 C 代码内存安全
satnam6502 · x · 2026-10-31
satnam6502 在格拉斯哥大学举办题为「为什么形式化验证世界正在火热」的研讨会,并透露更多细节:他使用形式化验证系统 Aristotle 成功证明了 OpenTitan 硅根信任(silicon root of trust)中部分 C 代码的内存安全性。
从配图截图可见, Aristotle Agent 已完成任务,对 otpctrlseccm 安全计数器的 7 条属性全部给出 Proved(0 条 Refuted),Agent 还能就 scope、断言选择、FSM 状态信号等技术细节提出追问并核对规则是否空泛成立。他表示后续会分享更多内容。
所属事件:Harmonic 工程师展示用 Aristotle 验证 OpenTitan 内存安全(3 条相关)→
「编程与Agent」频道最新
- GitHub Copilot 应用正开发仪表盘功能，可视化组件即将上线 — mariorod1 · 2026-10-31
- Todoist 搭建自愈系统：Agent 监控 Sentry 自动修 bug，五分之一免人工 — zeeg · 2026-10-31
- 独立开发晒 Multica 1.0 开发账单:4.3 亿 token 花 183 美元 — jiayuan_jy · 2026-10-31
- 游戏工作室让多台机器自动跑游戏回传 QA 报告 — draginol · 2026-10-31
- 开发者一年打造 Limma MCP:结构化全量数据,宣称检索零遗漏 — FlimsyIngenuity7248 · 2026-10-31
- Agent 审计新思路：不看总结，让用户说出改了哪些文件跑过哪些测试 — ronbodkin · 2026-10-31