English | 日本語

A Lean backend framework whose authorization safety is formally proven.

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 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.

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.

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.
4. Call it from any client. Clients call the backend over HTTP with a Supabase Auth JWT. The frontend lives outside Nyxis as an ordinary HTTP client.

An example schema (from the official bulletin-board sample):

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] };

An example policy:

// Only the author or an admin can edit, publish, or delete a post.
@id("manage-post")
permit (
  principal is User,
  action in [Action::"editPost", Action::"publishPost", Action::"deletePost"],
  resource is Post
) when { resource.author == principal || principal.admin };

Besides read, list, insert, update (with an explicit column list), and delete, effects include file storage via signed URLs, email notifications, and external API calls. All of them go through the authorization layer and are covered by the same theorem. Nyxis determines the principal from the JWT, the resource from the current database row, and the current time and unique IDs per request, so handlers cannot forge any of them.

• Lean 4 via 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

python3 scripts/prepare-dependencies.py   # fetch pinned dependencies into .lake/vendor/, verified by SHA256
lake build                                # build and check the core, proofs, and tests

See docs/dependencies.md for dependency preparation and docs/local-supabase.md for setting up a local Supabase (both in Japanese).

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):

require nyxis from "<path to your Nyxis clone>"

Link arguments for libpq do not propagate to the requiring package, so copy the postgresLinkArgs definition from the root lakefile.lean into your application's lakefile.lean. Declare the approved sources with nyxis_approved, and put nyxis_check_app at the end of a final module that imports every application module. See the official samples for the concrete layout.

• examples/bulletin-board/: 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/: document sharing within organizations, with memberships and roles, timestamps, filtered and paginated lists, attachments, email notifications, and external API calls. Backend only for now.

Apart from the README and ASSUMPTIONS, documentation is currently written in Japanese.

• ASSUMPTIONS.md: scope of the guarantee and the assumptions trusted outside the proof
• docs/proofs.md: catalog of proven theorems and what each one does not state
• docs/connection.md: how the connection code upholds the assumptions

MIT License © 2026 Nyx Foundation