Nyxisとは｜認可の安全性をLeanで形式証明したバックエンドフレームワーク

認可（authorization）の抜けは、AIにコードを書かせる開発でいちばん壊しやすい箇所だ。Nyxis（NyxFoundation/nyxis、★133・MIT・v0.1.1）は、その認可の安全性を Lean 4 で形式証明したバックエンドフレームワークである。開発者が書いて承認するのは Cedar のスキーマとポリシーだけで、ハンドラは Claude Code などの AI に書かせてよい。本記事は公式リポジトリの README・ASSUMPTIONS.md・docs/proofs.md を実読し、何が証明され、何が証明の外で信頼されているかを整理した（lake build の完全実行には到達していない範囲は後述する）。

Claude Code そのものの導入と運用はClaude Code｜2026年版・インストールからCLAUDE.md・Hooks・本番運用までの実装手引きにまとめている。本記事はその「AI に書かせたコードを安全に出す」側の一手段として Nyxis を扱う。

Nyxisとは｜AIが書いたバックエンドの認可をLeanで証明する

Nyxis が解くのは、個人開発者が AI にコードを書かせて Web アプリを出すときの「認可が本当に正しいか」という不安だ。README の主張を一文で言うと次になる。

ここで正当な権限を決めるのは、開発者が承認した Cedar のスキーマとポリシーである。Nyxis は従来の「認可ロジックを手書きし、テストで確からしさを積む」やり方を、「ポリシーを宣言し、それを超えないことを証明する」やり方に置き換える。「ハッキング不可能」や「完全に安全」という話ではない。証明が届くのは認可の範囲だけで、境界の外は別に信頼している（後述）。

技術スタックは Cedar（認可ポリシー言語）＋ Supabase（PostgreSQL と Supabase Auth の JWT）＋ Lean 4（lean-toolchain で v4.34.1 にピン留め、実測）。コアと証明は Nyxis/ にあり、主定理は Nyxis.Runtime.authorization_safety である。

仕組み：開発者はCedarだけ書き、ハンドラはAIに任せる

スキーマはテーブル定義を兼ねる。エンティティ型がテーブル、属性が列、エンティティ ID が主キーになり、各アクションには効果（permit されたとき DB で起きる操作）を 1 つ添える。公式サンプルの掲示板のスキーマはこう書く。

entity User = { "admin": Bool };
entity Post = { "author": User, "title": String, "body": String, "published": Bool };

@effect("update Post(title, body)")
action "editPost" appliesTo { principal: [User], resource: [Post] };

誰がそのアクションを通せるかはポリシーで宣言する。書かれていない操作は Cedar の既定どおりすべて拒否される。

// 投稿の編集・公開・削除は作者と管理者だけができる。
@id("manage-post")
permit (
  principal is User,
  action in [Action::"editPost", Action::"publishPost", Action::"deletePost"],
  resource is Post
) when { resource.author == principal || principal.admin };

ハンドラは Nyxis の Nyxis.Handler 型で書く。持てる効果は認可層へのアクション呼び出しだけで、IO や DB への直接到達はできない。主体は JWT から、対象は DB の現在の行から、現在時刻と一意 ID は要求ごとに Nyxis が決めるため、ハンドラはこれらを偽れない。効果の種類は read・list・insert・update（列を列挙）・delete に加え、署名付き URL によるファイル保管、メール通知、外部 API 呼び出しまで含み、いずれも同じ認可層を通って同じ定理の対象になる。だからハンドラの中身は AI に書かせてよい。越権は型と証明が塞ぐからだ。

Nyxisで証明されているのは認可の安全性だけ

lake build を通すと、ビルドと同時に承認したスキーマとポリシーへの結び付け、アプリケーションコードの監査、そして証明の検査が走る。主定理は Lean の項として書かれ、lake build のたびに Lean のカーネルがそれを検査する。Test/Axioms.lean が「全定理が標準の 3 公理（propext / Classical.choice / Quot.sound）以外に依存しない」ことまで確かめる。

結果として、認可のレビューと監査は「スキーマとポリシーを読み、証明が通っていることを確かめる」ことに帰着する。ハンドラ 1 本ずつを目で追って越権がないか探す作業は要らない。主定理 authorization_safety は、任意のアプリ・初期状態・認証済み要求列について、発行される全操作が主体の正当な権限の範囲内であること、状態遷移が記録と整合すること、ハンドラに渡る行が認可済み読み取りの指す行であること、一覧・連鎖削除・外部効果（署名 URL・メール・外部 API 呼び出し）までが同じ条件を満たすこと、を 9 つの結論として述べている。

ただし proofs.md は、この定理が述べていないことも明記している。たとえば HTTP・JWT・SQL との対応、サーバー生成値の一意性や時計の正しさ、署名付き URL の中身、メールや外部 API の配送の成否、そして「permit/deny の観測を含む無条件の非干渉」は主張に含まない。lake build が通ったことは認可の定理が通ったことを示すだけで、これだけで本番システム全体が安全とは言えない。

証明の外で信頼している前提を本番前に読む

この種のフレームワークの価値は、信頼境界を正直に引いているかで決まる。Nyxis は ASSUMPTIONS.md で、証明の外で信頼している前提を 3 つに整理している。

前提1は「証明の外で動くコード」だ。接続コードの一部（認証から主体を作る配線、1 要求＝新規接続 1 本の SERIALIZABLE トランザクション、応答の再生など）は証明済みで信頼対象から外れているが、生 HTTP の復号、PostgreSQL が SQL を実行したときの効果・分離性・永続化、curl の起動と応答解析などは実装済みでも未証明のまま残る。Lean カーネルや FFI、JWT 署名検証の暗号実装もここに入る。

前提2はクラウドサービスの振る舞いだ。たとえば「DB の行は Nyxis の専用ロールの操作以外では変わらない（Data API や他ロールからは触れない）」が崩れると、admin 列を裏口から true にするような操作は証明の外で起きる。前提3は開発者と運用者の正しい使い方だ。承認したスキーマとポリシーだけをデプロイする、接続文字列や service_role キーを漏らさない、ポリシーで宛先列や外部 API の送り先を最小に絞る、といった人の責任にあたる。ASSUMPTIONS.md は各前提に「破れたら何が起きるか」まで添えており、統合テストの成功を形式証明の代わりにしないと明言している。

試すには、必要なものとビルドと公式サンプル

Nyxis は Lake の require で取り込む独立パッケージだ。アプリ側のパッケージはスキーマ・ポリシー・ハンドラ・起動だけを持ち、Nyxis のコードは持たない。先にこのリポジトリを clone してビルドを済ませ、公式サンプルと同じくパスで require する。

# 依存を SHA256 で照合して .lake/vendor/ に置く → コア・証明・テストを検査
python3 scripts/prepare-dependencies.py
lake build

# アプリ側の lakefile.lean で require（libpq のリンク引数は伝わらないため postgresLinkArgs も複製する）
# require nyxis from "<clone した Nyxis へのパス>"

必要なものは、elan 経由の Lean 4（版は lean-toolchain で固定）、Python 3.12 以降・OpenSSL CLI・C コンパイラ、pkg-config と libpq・libcrypto の開発用ファイル、実行時に PostgreSQL（Supabase）と Supabase Auth。承認するスキーマとポリシーは nyxis_approved で宣言し、全モジュールを import した最終モジュールの末尾に nyxis_check_app を置く。

公式サンプルは 2 つ。examples/bulletin-board/ は投稿の公開・下書き、Google OAuth、管理者権限の付与と剥奪を備え、Next.js フロント付きで画面を操作しながらポリシーどおりの許可と拒否を体験できる。examples/team-docs/ は組織内の文書共有（所属・役割・添付・メール通知・外部 API 呼び出し）で、現状はバックエンドのみだ。

導入の判断：向いている人・待った方がよい人

Nyxis は「AI に書かせたハンドラの認可だけは機械で担保したい」個人開発者に向く。逆に、認可以外の安全性（可用性・機密性の別側面・配送保証）まで一枚で欲しい人や、Lean・Cedar・Supabase の前提を運用に載せる余力がない段階では、まだ早い。v0.1.1 で活発に開発中であり、ASSUMPTIONS.md の前提を読んで自分の運用に当てはめられるかが採用の分かれ目になる。

考え方をもう少し広く掴みたい場合は、AI にコードを書かせる開発そのものの全体像をVibe Codingとは？AIコーディングの始め方・ツール比較・実践ワークフロー2026で、Claude Code の基礎をClaude Codeとは？2026年版の実像で、運用のコツをClaude Code ベストプラクティスガイドで押さえておくと、Nyxis の立ち位置が理解しやすい。

まとめ

Nyxis は、「人が Cedar を承認し、証明が通ったものだけ出す」という線引きを形式手法で実装した初期の実例だ。AI がハンドラを書いても、越権は型と Lean の証明が塞ぐ。証明が届くのは認可の安全性に限られ、接続コードの一部・クラウド・処理系・運用は証明の外で信頼されている。その境界を ASSUMPTIONS.md が正直に引いている点にこそ読む価値がある。どこまでが証明でどこからが信頼かを読んだうえで採否を決めたい題材だ。

参照ソース

・NyxFoundation/nyxis（公式リポジトリ） — README・LICENSE・lean-toolchain・examples（2026-10-26 時点、★133 / fork 2、main は v0.1.1）
・ASSUMPTIONS.md — 保証の範囲と、証明の外で信頼する 3 つの前提
・docs/proofs.md — 証明している定理と、それぞれが述べないことの目録