**KERN：首个零信任 AI 代码验证网关，以形式化证明对抗幻觉**

_Kern – a zero-trust verification gateway for AI-generated code_

> KERN 是一款基于 Zig 和 Lean 4 构建的零信任验证网关，旨在解决 AI 生成代码难以被传统 CI 检测的问题。它利用 Z3 SMT 求解器和 Belnap B4 四值逻辑，将代码验证从简单的“通过/失败”升级为“已证明/已证伪/冲突/未知”。KERN 通过强制检查项必须具备可失败性（Can-fail discipline）和依赖机器合约（Machine contracts），能有效识别传统测试无法发现的“空洞测试”和“幻觉修复”，确保代码变更在机器证据确凿前不会合入仓库。

**来源信息**
- **来源**：Hacker News：AI 热帖
- **分类**：ai-products
- **发布时间**：2026-10-16 15:49（北京时间）
- **原文**：[打开原文](https://github.com/newmathphys/kern)