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

日本开发者开源了后端框架 Nyxis，用 Lean 形式化验证机械地证明了授权安全定理，任何 HTTP 请求序列都无法让已认证主体越权读取、修改、删除数据或授予权限。