Nyxis 开源：用 Lean 形式化证明保证 AI 写的后端不会越权泄露

udmrzn · x · 2026-10-28

日本开发者开源了号称世界首个「数学上保证不泄露机密信息」的后端框架 Nyxis（MIT 协议，GitHub 290 stars）。核心思路：AI agent（如 Claude Code）可以随意写 handler 代码，开发者只需管理「哪类用户能执行什么」的 Cedar schema 与策略，授权安全性由框架兜底。

框架大部分用 Lean 编写，通过形式化验证机械地证明了授权安全性定理：任何 HTTP 请求序列都无法让已认证主体越权读取、修改、删除数据或授予权限。作者指出授权缺陷在 OWASP 榜单自 2019 年起连续排第一，而对比微软/GitHub 新发布的 PDD Kit（需为每个程序写规格并人工确认），Nyxis 把定理预先固定为授权安全性，开发者只管策略即可。