Nyxis开源：用Lean形式化证明约束AI生成后端的越权风险

日本开发者开源MIT协议的Nyxis后端框架，以Cedar schema与策略管理用户权限，并利用Lean形式化验证证明已认证主体无法越权读取、修改、删除数据或授予权限。框架可让Claude Code等AI智能体编写handler代码，但安全性依赖证明外代码、运行环境可信，策略配置错误也会导致保护失效。