情報漏洩を防ぐ数学的保証！形式検証済みのLean製バックエンドフレームワーク「Nyxis」を徹底解説

Nyxis Lean FormalVerification Security Backend AI生成

2026年10月26日にNyx Foundationの柳浜万里氏（banri）が公開した、認可安全性をLean 4で形式証明したバックエンドフレームワーク「Nyxis」について、解決する課題、Cedarを用いた仕組み、主定理の内容、信頼する仮定（TCB）まで一次情報をもとに詳しく解説します。

:::message alert この記事はAIによって自動生成されたものであり、Daisukeが執筆したものではありません。公開前にDaisuke自身が内容のレビューを行っていますが、記載された情報の正確性や完全性を保証するものではありません。正確な情報については、記事末尾に記載している一次情報（公式リポジトリ・発表資料等）を必ずご確認ください。 :::

2026年10月26日、研究組織 Nyx Foundation の共同創業者であり Atlas Intelligence の技術顧問を務める柳浜万里氏（@banr1_）が、「情報漏洩が起きないことを数学的に保証する」 というバックエンドフレームワーク 「Nyxis」 をオープンソース（MITライセンス）として公開し、X（旧Twitter）を中心に大きな話題を呼んでいます。

Nyxis は定理証明支援系でありプログラミング言語でもある Lean 4（v4.34.1）で実装されており、「どのようなHTTPリクエスト列が送られても、認証された主体の正当な権限を超えるデータの読み取り・変更・削除・権限付与は発生しない」 という認可安全性（Authorization Safety）を機械的に形式証明したフレームワークです。開発者はポリシー記述言語 Cedar でスキーマとポリシーを書いて承認するだけで、残りのエンドポイント実装（ハンドラ）を Claude Code などの AI エージェントに任せても、認可の安全性が数学的に担保される設計になっています。

この記事では、公開された GitHub リポジトリ（NyxFoundation/nyxis）のソースコード、証明の目録（docs/proofs.md）、信頼する仮定の定義書（ASSUMPTIONS.ja.md）、および開発者の発表ポストなどの一次情報をもとに、Nyxis の仕組みと技術的なポイントを徹底解説します。

:::message 本記事の内容は 2026年10月26日 20時10分（JST）時点 の情報（v0.1.1）に基づいています。日時は原則として協定世界時（UTC）と日本時間（JST = UTC+9）を併記し、元ソースに時刻の記載がない日付のみの情報はそのまま記載しています。また、同名の別プロジェクト（UIツールキットの juliodaal/nyxis やバイナリシリアライゼーション形式の nyxis-io/nyxis など）とは無関係ですのでご注意ください。 :::

まずは結論から！Nyxis の要点まとめ

一言でいうと、「開発者が『誰に何を許可するか』のポリシーだけを管理すれば、AIがどんなハンドラを書こうと、権限外のデータアクセスが起きないことをビルドのたびに Lean のカーネルが数学的に検査してくれるフレームワーク」 です。

1. 背景：なぜ今「認可の形式検証」なのか？

OWASP Top 10 で長年1位を占める「認可の不備」

WebアプリケーションやAPIのセキュリティにおいて、「認証（Authentication：通信相手が誰であるかを確認すること）」以上に実装ミスが起きやすいのが 「認可（Authorization：そのユーザーが対象のデータに対してその操作を行う権限があるかを判定すること）」 です。

開発者の柳浜氏が発表ポストおよびリプライ（2026-10-26 09:58:17 UTC / 18:58:17 JST）で言及しているとおり、アクセス制御・認可の不備は業界標準の脆弱性ランキングにおいて最優先の課題であり続けています。

• OWASP Top 10（Webアプリケーション向け）：2021年版で「A01: Broken Access Control（アクセス制御の不備）」が1位となり、2025年版でも1位を維持。
• OWASP API Security Top 10（API向け）：2019年版・2023年版ともに「API1: Broken Object Level Authorization（BOLA：オブジェクトレベルの認可の不備）」が連続で1位。

一般的なWeb開発では、各エンドポイントのハンドラやコントローラの中で「ログイン中のユーザーIDと、取得・更新しようとしているレコードの所有者IDが一致するか」「管理者フラグが立っているか」といった if 文やクエリ条件を個別に記述します。しかし、機能追加や仕様変更のたびにチェック漏れ（たとえば一覧取得ではフィルタリングしているのに、個別取得や更新エンドポイントでチェックを忘れるなど）が発生しやすく、重大な情報漏洩の温床となってきました。

AIコーディング時代における「テスト」の限界

さらに近年、Claude Code などの AI エージェントにバックエンドの実装を任せる開発スタイルが急速に普及しています。AI は人間よりも高速に大量のコードを生成できる一方、数十〜数百のエンドポイントすべてにおいて認可の境界条件を1つも漏らさず実装し続けることは容易ではありません。

従来のソフトウェア開発では、こうしたバグを「テスト（単体テスト・結合テスト・ファジングなど）」で検出しようとしてきました。しかし、テストは「試した有限個の入力パターンで問題が起きなかったこと」しか確認できず、「未知の入力や複雑なリクエストの組み合わせ（リクエスト列）で絶対に権限逸脱が起きないこと」は証明できません。

2026年10月に相次いだ「AI × 形式検証」の潮流と Nyxis の立ち位置

2026年10月下旬、ソフトウェア業界では「AI時代のコードを形式検証（Formal Verification）でどう守るか」という発表が相次ぎました。柳浜氏も発表の中で、直近の2つの大きな取り組みと Nyxis の違いを明確に説明しています。

つまり、PDD Kit のように「関数・機能ごとに毎回どんな形式仕様を証明するか人間が悩む」のでも、Anthropic × Theorem のように「低レイヤーのバイナリがクラッシュしないことを大量の証明コードで示す」のでもなく、「Webバックエンドで最も致命的になりやすい『認可安全性』という1つの定理をフレームワークのコアであらかじめ完全に証明しておき、アプリケーション開発者はポリシー定義だけに集中できるようにした」 のが Nyxis の最大の発明です。

2. 公開までのタイムライン

リポジトリの履歴（ASSUMPTIONS.ja.md の来歴および Git コミットログ）と X 上の発表を時系列で整理すると、以下のようになります。

3. Nyxis のアーキテクチャと仕組み

Nyxis がどのようにして「開発者は Lean を1行も書かずに済むのに、AIが書いたバックエンドの認可安全性が Lean で証明される」という仕組みを実現しているのか、4つのステップに沿って見ていきましょう。

[1. 人間が書いて承認]
  ├─ schema.cedarschema （テーブル定義 ＋ 各アクションの @effect 宣言）
  └─ policies.cedar     （誰がどの条件でどのアクションを実行できるか）
          │
          ▼  nyxis_approved でビルド時に結合
[2. AIエージェントが実装]
  └─ Handlers.lean      （Nyxis.Handler 型の自由モナド。直接の IO や生 SQL は記述不可）
          │
          ▼  lake build（nyxis_check_app によるコード監査 ＋ Lean カーネルによる証明検査）
[3. 検証済みバックエンドバイナリ]
  └─ 1リクエスト ＝ 1本の SERIALIZABLE トランザクションで段階的実行（handleStaged）

ステップ1：Cedar を「唯一の正本（Single Source of Truth）」にする

Nyxis では、AWS が開発したオープンソースのポリシー記述言語 Cedar（およびその Lean 4 形式仕様である cedar-spec / cedar-lean）を認可エンジンとして採用しています。

重要な特徴は、Cedar のスキーマファイル（.cedarschema）がそのままデータベースのテーブル定義と ORM の役割を兼ねている点です。

• エンティティ型（entity）＝ PostgreSQL のテーブル
• 属性 ＝ テーブルの列（カラム）
• エンティティ ID ＝ 主キー（Primary Key）
• アクション（action）＝ 認可層に対する操作単位

さらに、各アクションには Nyxis 独自の注釈 @effect("...") で 「そのアクションが permit（許可）されたときにデータベースや外界で起きる効果」をちょうど1つだけ 宣言します。

Nyxis がサポートしている @effect の種類は以下のとおりです（Nyxis/Db.lean・Nyxis/CedarSchema.lean より）。

1. read <Table>：主キーによる単一行の読み取り
2. list <Table>：条件（フィルタ・ソート・ページング）に合い、かつ各行について permit された行の一覧取得
3. insert <Table>：新規行の挿入（提案される値が検査対象になる）
4. update <Table>(<col1>, <col2>, ...)：列挙されたカラムだけの更新（宣言していないカラムは絶対に書き換えられない）
5. delete <Table>：行の削除
6. upload <Table> / download <Table>：Supabase Storage のオブジェクト（テーブル/<主キー>/<名>）に対する署名付きURLの発行
7. mail <Table>(<宛先列>; <件名列>, <本文列>...)：対象行の指定カラムの値を宛先・件名・本文とする SMTP メール送信
8. call <送り先> <メソッド> <パス | url: 列> <Table>(<列>...) (sync [<秒>s] -> <型> | async)：@external で宣言した外部APIへのHTTP呼び出し（同期、または予約テーブル _nyxis_outbox を用いたトランザクション・アウトボックスパターンによる非同期送信）

また、スキーマには以下のような高度なリレーショナル制約や階層関係の注釈も記述できます。

• @unique("列, ...")：一意性制約（違反時は認可済みの操作についてのみ 409 Conflict）
• @references("列 restrict, 列 cascade アクション")：外部キー参照整合性と連鎖削除（cascade の場合、連鎖して消える子レコード1行ずつに対しても指定された削除アクションで Cedar の認可判定が行われ、1行でも拒否されればリクエスト全体が 403 Forbidden で拒否される）
• @parents("列") / @memberships("中間テーブル: 列 -> 列, ...")：組織やチームへの多対多の所属関係を Cedar のエンティティ階層（principal in resource.org など）として直接判定できる仕組み

ステップ2：ハンドラを自由モナド Nyxis.Handler に閉じ込める

エンドポイントの処理（ハンドラ）は、通常の IO モナドではなく、Nyxis が定義する帰納型（自由モナドの形）である Nyxis.Handler で記述します。実際の Nyxis/Handler.lean の定義は非常にシンプルです。

/-- ハンドラのプログラム。`pure` か、アクション呼び出し `call` の後に続きを待つかのどちらか。 -/
inductive Handler (α : Type) : Type where
  /-- 値を返して終わる。 -/
  | pure (a : α) : Handler α
  /-- アクション `action` を主キー `key` の行に、提案する値 `values` で呼び、結果を受けて続ける。 -/
  | call (action : EntityUID) (key : Db.Key) (values : Db.Row) (query : Db.ListQuery) (k : Outcome → Handler α) :
      Handler α

この型には IO を実行するコンストラクタも、生 SQL を発行するコンストラクタも存在しません。ハンドラができる唯一の副作用は「アクション名・主キー・提案する値（または一覧クエリ）を渡して認可層を呼ぶこと（Handler.callAction / Handler.callList）」だけです。

しかも、ハンドラは以下の重要な値を偽装・指定することが構造的に不可能になっています。

• 主体（Principal）：ランタイムが HTTP リクエストの Authorization: Bearer <JWT> を検証して決定する（ハンドラには Authorization ヘッダや Cookie ヘッダすら渡されない）。
• 判定対象のリソース（Resource）：ランタイムが DB の現在の行から直接構築する。
• サーバー生成値（context.now / context.id）：リクエストごとにランタイムが OS の時計と乱数源から1度だけ生成する現在時刻と UUID v4。
• 外部効果の宛先やURL：メールの宛先・本文や外部APIのURLは、スキーマの宣言と DB の対象行のカラム値からランタイムが決定するため、AIが書いたハンドラが勝手に外部の攻撃者サーバーへデータを送信することはできない。

ステップ3：lake build によるコード監査と証明検査

もし悪意のある（あるいはハルシネーションを起こした）AIエージェントが、Lean のメタプログラミング機能や FFI（外部関数インターフェース）を使って Handler の型制約を突破しようとしたらどうなるでしょうか？

これを防ぐため、Nyxis はビルド時に2つの仕組みを走らせます。

1. nyxis_approved による正本の結合：人間が承認した .cedarschema と .cedar をビルド時にパースしてアプリケーションの型に固定し、ルータやハンドラ側からはポリシーやスキーマを差し替えられないようにします。
2. nyxis_check_app によるエラボレーション後の全定数監査（Nyxis/AppCheck.lean）：アプリケーション側の最終モジュールで nyxis_check_app コマンドを実行すると、フレームワークの信頼済みモジュール以外のすべての定数を走査し、以下の要素が1つでも含まれていればビルドエラーとして拒否します。
   • unsafe 宣言、@[extern] 属性、@[implemented_by] 属性
   • 初期化処理（init）、マクロ・エラボレータ属性（macro / elab）
   • 禁止された定数への参照（dbgTrace*、panic*、ptrAddrUnsafe、unsafeCast、sorryAx、setImplementedBy）
   • lean-pq や Nyxis.Internal.* など外部機能を持つ内部モジュールの直接 import

さらに、Test/Axioms.lean の #assert_axioms_under Nyxis によって、Nyxis 内のすべての定理（公開定理 210 個・private 定理 31 個）が Lean の標準の3公理（propext / Classical.choice / Quot.sound）以外に依存していないこと（sorry などの未証明の穴がないこと）がビルドのたびに機械的に検査されます。

ステップ4：部分取得（Slicing）と SERIALIZABLE トランザクションによる実行

「DBの全行をメモリに読み込んで Cedar で判定する」のでは、テーブルが巨大になったときに実用的な性能が出ません。そこで Nyxis のランタイム（PostgresRun.handleStaged）は、1つのHTTPリクエストを PostgreSQL の新規接続1本の ISOLATION LEVEL SERIALIZABLE トランザクション として開始し、アクション呼び出しごとに以下の段階的な実行（Staged Execution）を行います。

1. 必要な判定材料だけの取得（PostgresMaterials.load）：主キーによる点検索や、必要な WHERE 句付き SELECT によって、そのアクションの認可判定に必要な行だけを DB から取得します。
2. 被覆検査（Authz.coversStep）と Slicing 定理：Cedar のポリシーがエンティティの属性を最大何段辿るか（レベル n）を静的に求め、要求から n 段で到達できる実体がすべて取得できているかを実行時に検査します。この検査に通れば、「部分的に取得した行だけで行った Cedar の認可判定が、DB全体の行を使って行った判定と数学的に完全一致すること」 が、cedar-lean の Slicing 定理（validate_with_level_is_sound_wf）を用いて証明されています（Nyxis/Materials.lean の isAuthorized_slice および Nyxis/Authz.lean の step_eq_of_covers）。
   • リポジトリの統合検査（scripts/check-materials-scale.py）では、User と Post に10万行を追加した状態でも、一覧以外の各リクエストが読む行数は空の状態と同じ（合計16行以内）で、応答時間の中央値も2倍以内に収まることが確認されています。
3. 操作の SQL 化と結果の照合（PostgresSql / PostgresWrite）：認可層が発行した操作だけをパラメータ化 SQL に変換して実行し、影響件数などが純粋モデル（Store.apply）の期待値と一致するかを照合します。不一致やエラーがあれば即座にロールバックし、詳細を隠した固定の 503 を返します。すべての段が成功し COMMIT が完了した後にのみ、HTTP レスポンスを返します。

4. コードで見る Nyxis の使い方（公式サンプル「掲示板」より）

リポジトリの examples/bulletin-board/ に収録されている公式サンプル（Next.js フロントエンド付きの掲示板アプリ）から、実際のコードを見てみましょう。

① スキーマの定義（schema.cedarschema）

人間が書いて承認する1つ目のファイルです。テーブル構造と、各アクションが持つ @effect を宣言します。

// 利用者。Supabase Auth のユーザー ID がエンティティ ID(主キー)になる。
entity User = {
  "admin": Bool
};

// 投稿。
entity Post = {
  "author": User,
  "title": String,
  "body": String,
  "published": Bool
};

// 匿名の主体(nyxis が予約。テーブルではない)。
entity Anonymous;

// 投稿を読む。
@effect("read Post")
action "readPost" appliesTo {
  principal: [User, Anonymous],
  resource: [Post]
};

// 投稿の一覧。
@effect("list Post")
action "listPosts" appliesTo {
  principal: [User, Anonymous],
  resource: [Post]
};

// 投稿を作成する。
@effect("insert Post")
action "createPost" appliesTo {
  principal: [User],
  resource: [Post]
};

// 投稿の題名と本文を編集する（author や published は変更不可）。
@effect("update Post(title, body)")
action "editPost" appliesTo {
  principal: [User],
  resource: [Post]
};

// 利用者を登録する(自分自身の User 行を admin=false で作る)。提案される値は context.values。
@effect("insert User")
action "registerUser" appliesTo {
  principal: [User],
  resource: [User],
  context: { "values": { "admin": Bool } }
};

たとえば editPost には @effect("update Post(title, body)") と書かれているため、仮にハンドラ側で author や published カラムを書き換える提案値を渡したとしても、宣言された効果の範囲外となり書き換えは発生しません。

② ポリシーの定義（policies.cedar）

人間が書いて承認する2つ目のファイルです。Cedar の原則により、明示的に permit されていない操作はすべて拒否（デフォルト deny）されます。

// 公開済み投稿は匿名を含む誰でも読める。
@id("read-published-post")
permit (
  principal,
  action in [Action::"readPost", Action::"listPosts"],
  resource is Post
) when { resource.published };

// 下書きの投稿は作者と管理者だけが読める。
@id("read-draft-post")
permit (
  principal is User,
  action in [Action::"readPost", Action::"listPosts"],
  resource is Post
) when { resource.author == principal || principal.admin };

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

// 自己登録時に自分で admin=true にすることを防ぐ。
@id("register-self")
permit (
  principal is User,
  action == Action::"registerUser",
  resource is User
) when { resource == principal && context.values.admin == false };

③ ハンドラの実装（BulletinBoard/Handlers.lean）

ここは AI エージェント（Claude Code など）に任せてよい部分です。認可の if 文は一切登場せず、Handler.callAction を呼んで結果を HTTP ステータスに写すだけです。

/-- `GET /posts` — 各行の認可を通った投稿だけを一覧にする。 -/
def listPosts : Principal → Generated → Http.Request → Handler Http.Response := fun _ _ _ => do
  let outcome ← Handler.callAction (act "listPosts") ""
  pure (respond .ok (fun _ => "") outcome)

/-- `PATCH /posts/{id}` — 題名・本文を編集する。本文にある列だけを変える。 -/
def editPost (id : Key) : Principal → Generated → Http.Request → Handler Http.Response := fun _ _ req => do
  let parsed : Except String Row := do
    let json ← parseObject req.body
    let title ← stringField json "title"
    let body ← stringField json "body"
    if title.isNone && body.isNone then throw "title or body expected"
    pure (rowOf [("title", title), ("body", body)])
  match parsed with
  | .error e => pure (badRequest e)
  | .ok changes => noContent <$> Handler.callAction (act "editPost") id changes

5. 主定理 authorization_safety は何を数学的に保証しているのか？

Nyxis/Runtime.lean で証明されている主定理 Nyxis.Runtime.authorization_safety（および承認済み正本に特殊化した Nyxis.Approved.authorization_safety）は、任意のアプリケーション app、任意の初期DB状態 store、任意の認証済みリクエスト列 requests（定期処理の起動を含む）を順に処理した結果 trace app store requests について、以下の 9つの性質すべての連言（AND） が成り立つことを証明しています。

1. 正当な権限（trace_authorized）：発行されたすべてのDB操作は、そのリクエストの認証された主体とサーバー生成値に一致し（偽装できず）、スキーマで宣言された効果の範囲内にあり、その時点のDB状態に対して Cedar ポリシーが permit と判定したものである。
2. 状態遷移との整合（trace_coherent）：DBの状態は、(1)で正当と判定され記録された操作の適用（Store.apply）だけで変化し、各認可判定はその操作の直前の実際の状態に対して行われる。
3. ハンドラに渡る行の出所（trace_entries）：単一読み取りや一覧取得でハンドラ（ひいてはHTTPレスポンス）に渡った (主キー, 行) の組は、同じリクエストで permit されたその主キーの読み取りが指す現在の行に限られる（別の行の主キーと中身を組み合わせることもできない）。また、Nyxis/ReadSafety.lean の定理により、認可判定のために内部で取得した他の行がレスポンスに漏れる経路がないことも証明されている。
4. 一覧の件数とページ（trace_list）：一覧取得の件数（total）と返却される行（rows）は、対象テーブルのうちクエリの絞り込み条件に合い、かつその主体に permit された行（候補 permittedRows）だけから決まる。ページング（limit / offset）は permit された行に対して適用されるため、拒否された行の分だけページが欠けることもない。
5. 判定アクションの由来（trace_origin）：発行された各DB操作を判定したアクションは、ハンドラが呼んだアクションか、スキーマの @references（cascade）が宣言した連鎖削除のアクションのいずれかである。
6. 外部効果の記録（trace_external）：記録されたすべての外部効果（Storage の署名付きURL発行、メール送信、外部API呼び出し）は、対象行の読み取りと同じ判定材料（および提案値）で permit され、その内容はスキーマ宣言と対象行のカラム値・生成値から Nyxis が決定したものである。
7. 署名付きURLの由来（trace_signed）：ハンドラに渡った署名付きURLには、同じリクエストのその呼び出しについて記録された(6)の認可済み外部効果が必ず対応する。
8. 外部API呼び出しの内容の由来（trace_call）：記録された外部API呼び出し（sync / async とも）の送り先・メソッド・URL・本文は、スキーマの @external および @effect("call ...") の宣言と、対象行の宣言されたカラム、および context.values の判定を通った提案値だけから決まる。アウトボックス（_nyxis_outbox）に書かれる各行もこの記録そのものである。
9. 外部API応答の由来と非干渉（trace_called）：ハンドラに渡った外部APIの応答値には認可済みの呼び出し記録が対応し、外部APIがどんな応答値を返しても認可判定を変えない（step_external_indep）。その応答値をDBに保存するには、ハンドラが別のアクション（例：公式サンプル team-docs の recordSummary）を呼ぶ必要があり、再び(1)の認可判定を通る。

6. 証明の境界線：何を信頼しているのか（ASSUMPTIONS）と現在の制約

形式検証において最も重要なのは、「何が証明されていて、何が証明の外側の仮定（Trusted Computing Base: TCB）なのか」を誠実に開示することです。Nyxis は ASSUMPTIONS.ja.md と docs/proofs.md において、保証の3層（①純粋モデルで証明済み、②接続コードのうち証明済み、③未証明で信頼する仮定）を極めて詳細に文書化しています。

証明の外側で信頼する3つの仮定（Assumption 1〜3）

1. Assumption 1：証明の外で動くコード（接続コードの一部・ツールチェーン・FFI・暗号）
   • JWT から主体を作る配線や、段階的実行（handleStaged）で認可済み操作から SQL を生成し照合する流れ、外部効果を認可済み記録についてのみ呼ぶ配線などは接続コード側でも定理として証明済みです（docs/proofs.md）。
   • 一方で、生の HTTP 通信の復号・送信、点検索や WHERE 句付き SELECT の結果が外部 PostgreSQL の現在の行と一致すること（PostgresRun.Chain）、PostgreSQL が SQL を実行したときの意味論や永続化、JSON パーサ、curl プロセスの起動、アウトボックスの送出ループ（Outbox.loop）、Lean 4 コンパイラ／カーネル、lean-pq（libpq）、lean-jose（OpenSSL libcrypto）などの実装の正しさは証明の外側で信頼しています（統合テスト群で検証）。
2. Assumption 2：クラウドと実行環境
   • Supabase Auth が本人確認（OAuth）を終えたユーザーにのみ正しい sub の JWT を発行すること。
   • PostgreSQL に Nyxis 専用ロール以外からアクセスされないこと（Supabase の Data API / PostgREST 等を無効化すること）。
   • Supabase Storage（署名付きURLの検証）、前段のリバースプロキシ（TLS終端）、SMTP中継、外部APIの送り先、通信経路の TLS、OSの時計（NTP同期）と乱数源が仕様通りに動くこと。
3. Assumption 3：アプリの開発・運用者の正しい活用
   • 人間が Cedar のスキーマとポリシーを読んで意図通りか承認すること（ポリシー自体を誤って「全員に公開」と書けば、証明は通ったまま全員に公開されます）。
   • nyxis_approved と nyxis_check_app を含めて lake build を通したバイナリだけをデプロイすること（なお、nyxis_check_app はエラボレーション後の定数監査でありビルド時のサンドボックスではないため、監査到達前のビルド時 IO や main 関数の内容は信頼する必要があります）。
   • DB接続文字列や API キーなどのシークレットを秘匿し、クラウド側（OAuth 限定、Data API 閉鎖、Storage バケット非公開など）を正しく設定すること。

定理が述べないこと・現時点での制約と今後の課題

開発者の柳浜氏も発表ポストで「表現力の乏しさやLeanのライブラリ不足など、改善すべき点はまだ山積みです」と述べているとおり、現時点（v0.1.1）では以下のような制約や未決事項（ASSUMPTIONS.ja.md・docs/external-calls.md §7）があります。

• 無条件の非干渉（Non-interference）までは主張しない：たとえば一意性制約や参照整合性の違反（409 Conflict）は、permit された操作についてのみ発生しますが、permit された主体に対して「同じ値を持つ行や参照している行が存在する」という事実をステータスコード経由で伝え得ます。また、タイミング等のサイドチャネルも対象外です。
• インバウンド Webhook（外部サービスからのコールバック受信）が未対応：現在サポートしている外部API連携はバックエンドからの送信（sync / async）のみで、JWT を持たない外部サービスからの署名付き Webhook 受信は今後の検討課題とされています。
• 外部API呼び出しのクエリ文字列：@effect("call ...") のパスには {key}（主キー）以外のプレースホルダや ? / # を含められないため、GET /v1/search?q=... のようにクエリ文字列が必須の外部APIは当面対象外です。
• クエリやデータ型の表現力：Cedar のスキーマ＝テーブル定義という1対1対応により証明の見通しを良くしている反面、複雑な JOIN や集計クエリ、配列の配列など Cedar の型で表現できない構造には制約があります。

まとめ

Nyxis は、「人間はビジネスルール（誰に何を許可するかという Cedar ポリシー）の定義と承認に集中し、面倒なハンドラ実装は AI エージェントに任せ、その間の安全性（権限外のデータアクセスが起きないこと）は定理証明支援系 Lean 4 のカーネルに機械的に保証させる」 という、AIコーディング時代の理想的な役割分担を具現化したフレームワークです。

これまで形式検証は、暗号ライブラリやOSカーネル、ブロックチェーンのコアプロトコルなど、専門の研究者が膨大なコストをかけて適用する領域と思われがちでした。しかし Nyxis のように「フレームワーク側で普遍的なセキュリティ定理をあらかじめ証明しておき、一般的な Web 開発者が Lean の証明を書かずにその恩恵を受けられる」というアプローチは、今後のセキュアな Web バックエンド開発や AI エージェント活用のあり方に大きな示唆を与えてくれます。

リポジトリには Next.js フロントエンド付きの掲示板サンプル（examples/bulletin-board/）や、組織・ロール・添付ファイル・メール通知・外部API連携まで備えた文書共有サンプル（examples/team-docs/）が同梱されており、ローカルの Supabase 環境ですぐに試すことができます。興味のある方はぜひ公式リポジトリの README.ja.md や ASSUMPTIONS.ja.md を覗いてみてください。

参考資料・一次情報一覧

• 公式 GitHub リポジトリ
  • NyxFoundation/nyxis（リポジトリトップ）
  • README.ja.md（日本語 README）
  • ASSUMPTIONS.ja.md（証明の外側で信頼する仮定・保証の範囲）
  • docs/proofs.md（証明している定理と述べないことの目録）
  • docs/connection.md（仮定を支える接続コードの作り）
  • docs/external-calls.md（外部 API 呼び出しの設計）
  • Nyxis/Runtime.lean（主定理 authorization_safety の定義と証明）
  • GitHub Releases（v0.1.0 / v0.1.1）
• 開発者・関連組織の公式発表
  • 柳浜万里氏（@banr1_）による Nyxis 公開発表ポスト（2026-10-26 08:43:45 UTC / 17:43:45 JST）
  • 柳浜万里氏による OWASP Top 10 / API Security Top 10 に関する補足ポスト（2026-10-26 09:58:17 UTC / 18:58:17 JST）
  • 柳浜万里氏による Anthropic×Theorem 共同研究との違いに関する補足ポスト（2026-10-26 10:20:54 UTC / 19:20:54 JST）
  • Atlas Intelligence（@AtlasInt_Inc）による発表ポスト（2026-10-26 09:36:29 UTC / 18:36:29 JST）
  • Nyx Foundation 公式サイト
  • Atlas Intelligence 公式サイト
• 関連技術・比較対象の一次情報
  • Cedar Policy Language 公式サイト / cedar-policy/cedar-spec（Lean 4 による Cedar の形式仕様と証明）
  • LLMs are making formal software verification feasible at a much larger scale（Anthropic / Theorem、2026-10-22）