rv_inc 用 Lean 4 证明 89 条定理，顺带揪出一个 Linux 内核静默 bug
tianyin_xu · x · 2026-10-08
RV（rvinc）团队公开了对 Linux 内核隔离机制的形式化验证技术报告：
- 在 Lean 4 中证明了 89 条定理
- 规约过程中暴露了一个内核自身的静默 bug，并已提交内核补丁
- 过程中还把形式化验证工具 Aeneas 弄崩了，一并给出修复
转发者 Grigore Rosu（RV 创始人、K 运行时框架作者）评论称形式化验证 Linux 总能挖出有趣的东西——bug 既在内核里，也在验证工具里，欢迎做形式化验证的人加入挑战。
「研究」频道最新
- CoBPE 分词法让序列缩短 30%，同等算力下 LLM 效果更好 — alisawuffles · 2026-10-08
- 一批 SOTA 级决策与嵌入模型陆续开源 — antoine_chaffin · 2026-10-08
- DeCoPrune 免训练剪枝 85% 视频 KV 缓存，续写生成提速 4 倍 — mmlab-ntu · 2026-10-08
- 重审 2021 年起飞速度之辩：AI 分析称 Yudkowsky 数学对、Christiano 经济对 — jessi_cata · 2026-10-08
- Nature 子刊聚焦裸盖菇素研究:ML 揭示大脑'嵌入性'状态 — adeelrazi · 2026-10-08
- 后量子非交互式密钥交换 MIKE 开源,公钥最小仅 80 字节 — jedisct1 · 2026-10-08