NyxFoundation/nyxis

选用指南

AI 根据 README 整理 · 2026/10/26 18:31:26

适用场景

适用于需要严格授权保证的 AI 生成 Web 应用后端，如公告板、团队文档共享等场景。

查看 README 依据

Nyxis lets solo developers who ship web applications written by AI agents release them with confidence about authorization. The only things a developer writes and approves are a [Cedar](https://www.cedarpolicy.com/) schema and policies. Handlers can be written as usual by Claude Code or similar tools, and the developer never has to write Lean. Every backend built on Nyxis comes with a formal proof of the following: > No sequence of HTTP requests can cause an authenticated principal to read, modify, delete, or grant access to data beyond its legitimate permissions.

- [`examples/bulletin-board/`](examples/bulletin-board/README.md): a bulletin board with published and draft posts, Google OAuth login, and granting and revoking admin rights. It ships with a Next.js frontend, so you can watch the policies allow and deny requests as you use the UI. - [`examples/team-docs/`](examples/team-docs/README.md): document sharing within organizations, with memberships and roles, timestamps, filtered and paginated lists, attachments, email notifications, and external API calls. Backend only for now. ## Repository layout | Path | Contents | |---|---|

目标用户

面向使用 AI 代理编写 Web 应用、但需要授权安全验证的独立开发者。

查看 README 依据

Nyxis lets solo developers who ship web applications written by AI agents release them with confidence about authorization. The only things a developer writes and approves are a [Cedar](https://www.cedarpolicy.com/) schema and policies. Handlers can be written as usual by Claude Code or similar tools, and the developer never has to write Lean. Every backend built on Nyxis comes with a formal proof of the following: > No sequence of HTTP requests can cause an authenticated principal to read, modify, delete, or grant access to data beyond its legitimate permissions.

使用方式

通过 Lake 的 require 命令集成到应用中，使用 Lean 语言编写模式、策略和处理器，通过 lake build 构建并验证证明。

查看 README 依据

Nyxis is a standalone package you pull in with Lake's `require`. Your application package contains only the schema, policies, handlers, and startup code, and none of Nyxis's code. Nyxis resolves its pinned dependencies from `.lake/vendor/` inside its own checkout, so first run the build steps above in a clone of this repository, then require it by path (as the official samples do): ```lean require nyxis from "<path to your Nyxis clone>" ```

1. **Write and approve a Cedar schema and policies.** The schema doubles as the table definition (entity type = table, attribute = column), and each action carries exactly one effect defined by Nyxis. 2. **Write handlers (or let an AI agent write them).** Handlers have the Nyxis type `Nyxis.Handler`, and their only effect is calling actions on the authorization layer. They cannot perform IO or reach the database directly. 3. **Run `lake build`.** Building also binds the app to the approved sources, audits the application code, and checks the proofs.

部署要求

需要 Lean 4（版本已固定）、Python 3.12 或更高版本、OpenSSL CLI、C 编译器、pkg-config、libpq 和 libcrypto 开发文件，以及运行时依赖 PostgreSQL（Supabase）和 Supabase Auth。

查看 README 依据

# Nyxis English | [日本語](README.ja.md) [](LICENSE) [](https://github.com/NyxFoundation/nyxis) [](ASSUMPTIONS.md) [](lean-toolchain) [](https://www.cedarpolicy.com/)

cannot forge any of them. ## Requirements - Lean 4 via [elan](https://github.com/leanprover/elan) (the version is pinned in `lean-toolchain`) - Python 3.12 or later, the OpenSSL CLI, and a C compiler - pkg-config and the development files for libpq and libcrypto (on macOS, `brew install libpq`; because Homebrew's libpq is keg-only, add `$(brew --prefix libpq)/lib/pkgconfig` to `PKG_CONFIG_PATH`) - At runtime: PostgreSQL (Supabase) and Supabase Auth ## Build ```sh python3 scripts/prepare-dependencies.py # fetch pinned dependencies into .lake/vendor/, verified by SHA256

已知限制

Nyxis 正处于积极开发中（v0.1.1），保证范围和在证明之外信任的假设在 ASSUMPTIONS.md 中说明，生产使用前需阅读。

查看 README 依据

The Lean kernel checks this property on every `lake build`. Reviewing and auditing authorization comes down to reading the schema and policies and confirming that the proof checks. > [!NOTE] > Nyxis is under active development (v0.1.1). The scope of the guarantee and the assumptions trusted outside the proof are spelled out in [ASSUMPTIONS.md](ASSUMPTIONS.md). Read it before using Nyxis in production. ## How it works