2026年10月26日、「情報漏洩が起きないことを数学的に保証するバックエンドフレームワーク」としてNyxis（ニクシス）が公開されました。X（旧Twitter）では公開当日から大きく拡散しています。
「数学的に保証」という言葉はとても強いです。そのぶん、「Nyxisを使えば情報漏洩はゼロになる」と受け取られてしまう心配もあります。
そこで、GitHubで公開されているREADMEと、保証の範囲をまとめたドキュメント（ASSUMPTIONS.md）を実際に読んでみました。この記事では、何が証明されていて、何が証明の外にあるのかを整理します。
※この記事は2026年10月28日時点（Nyxis v0.1.1）の公開情報をもとにしています。開発中のプロジェクトなので、内容は今後変わる可能性があります。
Nyxisとは何か
Nyxisは、一般社団法人Nyx Foundation（東京都文京区）が公開したバックエンドフレームワークです。Nyx FoundationはEthereumの形式検証やセキュリティを専門にする研究組織で、MITライセンスのオープンソースとして公開されています。
特徴をひと言でいうと、「認可（誰が何をしてよいか）の安全性を、Leanという言語で数学的に証明している」フレームワークです。
開発の流れは次のとおりです。
- 開発者がルールを書く：Cedar（AWSが開発した認可ポリシー言語）で、データの形（スキーマ）と「誰が何をしてよいか」（ポリシー）を書き、人が承認します。
- 処理はAIに任せてもよい：実際の処理（ハンドラ）は、Claude Codeなどのコーディングエージェントに書かせても構いません。開発者がLeanを書く必要はありません。
- ビルドで証明を検査する：ビルドのたびに、証明が成り立っているかが自動で検査されます。
ポイントは、ハンドラがデータベースや外部に直接触れられない設計になっていることです。データへの操作は必ず認可の仕組みを通ります。ユーザーが誰かはログイン時のトークン（JWT）から、時刻やIDはサーバー側で決まるので、ハンドラが偽装することもできません。
そのため、AIが書いたコードに認可のチェック漏れがあっても、権限外の操作は通らない、というのがNyxisの考え方です。
証明されていること：認可の不備を構造的に潰す
READMEによると、Nyxisで作ったバックエンドには次の性質が証明されています。
「どんなHTTPリクエストの並びでも、認証済みのユーザーが正当な権限を超えてデータを読む・変更する・削除する・権限を付与することは起きない」
これはかなり価値のある性質です。Webアプリの脆弱性ランキングとして有名なOWASP Top 10では、「アクセス制御の不備（Broken Access Control）」が2021年版・2025年版と連続で1位になっています。他人のIDを指定すると他人のデータが見えてしまう、といった問題です。
通常の開発では、こうした不備はテストやレビューで見つけるしかありません。テストは「試したケース」しか確認できないので、抜け漏れは残ります。
Nyxisは「どんなリクエストの並びでも」成り立つことを証明しているので、テストでは拾いきれない抜け道まで含めて、認可の逸脱を構造的に防げるというわけです。ここは素直にすごい点だと思います。
証明の外にあるもの：3つの前提
一方で、この証明には範囲があります。これは批判ではなく、作者自身がASSUMPTIONS.mdで丁寧に書いていることです。
まず大事なのは、証明されているのが「ランタイムの純粋なモデル」の上での性質だという点です。実際に動くときには、モデルの外にあるコードや環境を信頼する必要があります。ASSUMPTIONS.mdでは、それを3つの前提にまとめています。
前提1：証明の外で動くコード
HTTPの受け取り、PostgreSQLとのやりとり、JSONの解析、署名検証などの暗号処理、Lean自体のコンパイラなどです。Nyxisの接続コードは一部が証明済みですが、未証明の部分も残っていて、ここは「正しく動く」と信頼する前提になっています。
前提2：クラウドサービスと実行環境
ログイン（Supabase Auth）、データベース、ファイル保存、メール送信、TLS、サーバーの時計などです。たとえば認証サービスが別人にトークンを発行してしまえば、Nyxisはその人を本人として扱います。証明ではその違いを見分けられません。
前提3：開発者・運用者の正しい使い方
承認したポリシーをそのままデプロイすること、秘密情報（DBの接続文字列やAPIキー）を漏らさないこと、クラウド側の設定を正しくすることなどです。たとえばDBの接続文字列が漏れれば、Nyxisを通らずに全データへアクセスできてしまいます。
一番の落とし穴：ポリシーが間違っていたら？
個人的に、いちばん誤解されやすいと感じたのがここです。
Nyxisの定理は「どんなスキーマとポリシーに対しても」成り立ちます。そして「正当な権限」が何かは、そのポリシーが決めます。
つまり、ポリシーを間違えて「一般ユーザーも管理者データを読める」と書いてしまった場合、それはNyxisにとって「正当な権限」になります。証明は成り立ったまま、意図しない情報が見えてしまいます。ASSUMPTIONS.mdにも、承認されていないポリシーがデプロイされれば、意図しない権限が「正当」になると明記されています。
整理すると、Nyxisが保証するのは次のことです。
- 保証される：実装（AIが書いたコードを含む）が、ポリシーから逸脱しないこと
- 保証されない：ポリシーそのものが、人間の意図どおりに正しいこと
作者も投稿の中で「開発者がポリシーを誤って書けば、意図した保護は得られない」と書いています。Nyxisを使うと、認可のレビューで見るべき場所が「全コード」から「スキーマとポリシー」に絞られる、と捉えるのが正確だと思います。それ自体は大きな前進です。
ネットワークエンジニアの目線で見る前提
ASSUMPTIONS.mdを読んで面白かったのは、前提の多くがインフラやネットワーク側の話だったことです。ネットワークエンジニア（以下、NE）として普段触っている領域が、そのまま「証明の外」に並んでいます。
- TLS終端とフロントのプロキシ：Nyxisのバックエンドは平文のHTTPで待ち受けるので、前段にTLSを終端するリバースプロキシやロードバランサーを置く前提です。そのプロキシがヘッダーや本文を書き換えないことも前提になっています。
- バックエンドに直接届く経路をなくす：バックエンドのポートは前段以外に公開しない前提です。直接届く経路があれば、平文のHTTPがTLSの外にさらされます。
- DBへの到達経路：データベースはNyxis専用のロールからしか操作できない前提です。SupabaseのData APIを無効化するなど、別の入口をふさぐ必要があります。
- 時刻同期（NTP）：トークンの有効期限の判定に時計を使うので、時計がずれると期限切れのトークンが通る可能性があります。
- 外向き通信とTLSの検証：公開鍵（JWKS）の取得やメール送信で外部と通信します。証明書の検証やCAの設定が正しいことも前提です。
つまり、アプリが数学的に証明されていても、ネットワークを雑に組めば保証は崩れます。ポートの公開範囲、経路の制御、時刻同期といった地味な設計が、そのまま「数学的保証」の土台になっているわけです。
これは、どれだけ堅いアプリでも、インフラの設定ミスや認証情報の漏洩には無力だという、これまでと同じ話でもあります。ちなみにOWASP Top 10 2025では「セキュリティの設定ミス」が2位に上がっています。
まとめ：テストより強い。でも「漏洩ゼロ」ではない
調べてみた結論をまとめます。
- 「数学的に保証」は本当：ただし対象は「認可の逸脱が起きないこと」で、しかもランタイムの純粋なモデルの上での話です。
- 認可の不備には非常に強い：AIにコードを書かせる時代に、「実装がポリシーを破らない」ことを証明できるのは大きな価値です。
- 「情報漏洩ゼロ」ではない：ポリシーの誤り、秘密情報の漏洩、インフラの設定ミス、外部サービスの不具合は保証の外です。
- まだv0.1.1：作者も、表現力の不足やLeanのライブラリ不足など、改善点が多いことを認めています。本番での採用は、ASSUMPTIONS.mdを読んでから判断するのがよさそうです。
形式検証が実用的なWebバックエンドにここまで近づいたこと自体は、とても面白い動きだと思います。一方で、「数学的に保証」という言葉だけが一人歩きしないように、何が保証されているのかを読む側も意識しておきたいところです。
なお、私は形式検証の専門家ではありません。読み違いや誤りがあれば、X（@ponflog）で教えてもらえるとうれしいです。確認のうえ、記事を修正します。
