核心内容
Runtime Verification 的 Grigore Roșu 与 Everett Hildenbrandt 在 Cognitive Revolution 直播中介绍如何把形式化方法与大模型结合：先为 Linux 内核模块编写严密规格，再用 LLM 辅助将 C 移植到 Rust 并进行差分模糊测试与形式化证明，从而在两阶段各发现真实漏洞。
Roșu 认为未来 AI 应同时生成代码、形式化规格与正确性证明，人类在环专注核对意图；主持人 Nathan Labenz 亦在开场分享智能体越权案例并强调人工接管机制。
Grigore Roșu and Everett Hildenbrandt of Runtime Verification join Nathan Labenz on Cognitive Revolution to describe combining formal methods with LLMs—writing formal specifications for Linux kernel components, translating C to Rust, and running differential fuzzing and formal proofs to uncover real vulnerabilities.
Roșu envisions AI generating code, specifications, and proofs together while humans verify intent; Labenz also discusses human override mechanisms for autonomous agents.
介绍依据 · 发布方说明 · 完整内容待核读
编辑导览，依据原始来源 ↗，整理于 2026-10-18。中英文均由本站概括整理。 内容介绍与下方原话、主张的逐条核对分开标注。
- 收录2026-10-17
- 逐字稿自动字幕
- 二次核对等人听原片
- 提炼未开始
采集库里有自动字幕。机器识别，人名和数字常错；要加引号，得先听原片登记二次核对。 原话怎么核对 →
收录说明：2026-10-12 直播，10-17 补齐自动字幕并通读前 44 分钟（全片约 3 小时）；仍待听校。
相关
Nathan Labenz：智能体隐蔽合谋、前沿全功能教师模型与安全收敛
Nathan Labenz·Cognitive Revolution·播客 · 2026-09-27
同一讲者已核对原话
中国行第三集：中美关系与机器人时代的秩序
Nathan Labenz·Cognitive Revolution·播客 · 2026-09-10
同一讲者已核对原话
Clark Barrett 与 Mykel Kochenderfer：代码形式化证明智能体与高可靠系统验证
Clark Barrett · Mykel Kochenderfer·YC Paper Club·演讲 · 2026-10-17
同话题 · 软件与编程
Latent Space 六人圆桌：OpenAI DevDay 新产品实测，什么真正可用？
Swyx·Latent Space·圆桌 · 2026-10-16
同话题 · 软件与编程
Greg Brockman：网络安全攻防转换、防御者窗口与科学发现
Greg Brockman·No Priors·播客 · 2026-10-15
同话题 · 智能体落地