nyxfoundation/nyxis は Cedar スキーマとポリシーに従ってアクセス権限を検査する Lean バックエンドフレームワークである。開発者は Cedar スキーマとポリシーを記述し、リクエスト処理には Supabase Auth と PostgreSQL を使用する。最新リリースは v0.1.9 である。提供された資料にはこのバージョンで変更された内容が記録されていないため、具体的な変更点は確認できない。
核心は Cedar ポリシーに基づく認可の挙動を形式証明で保証する設計にある。形式証明とは、定められた規則が成立するかどうかを数学的論理に従って確認する手法である。README によれば、リクエストハンドラの型は認可層の操作だけを呼び出すよう制限されており、ビルドの過程で証明とアプリケーション検査を実行する。中核実装と 2 つのサンプルバックエンドは Lean プロジェクトとして構成され、証明・依存関係・接続に関する文書も提供されている。リポジトリのライセンスは MIT である。
ただし README はプロジェクトが開発中である旨を明示しており、実際の保証範囲と証明に含まれない仮定については別の文書を参照するよう案内している。したがって、権限制御の保証に関する主張をシステム全体の安全性まで広げて解釈してはいけない。現在の資料では v0.1.9 の変更履歴も確認できないため、保証の境界とバージョンごとの差異は関連文書を通じて確認する必要がある。