v0.1.1

Changes

• README: Nyxis is now described as a backend framework. The English tagline reads "A Lean backend framework whose authorization safety is formally proven", and the Japanese README uses "バックエンドフレームワーク" in place of "Web バックエンド基盤".
• Version bumped to v0.1.1 in lakefile.lean and the README badges.

No changes to the framework code, proofs, or samples.

v0.1.0

First public release of Nyxis, a Lean web backend framework whose authorization safety is formally proven.

You write and approve a Cedar schema and policies; handlers (written by you or by an AI agent such as Claude Code) can only act through the authorization layer. Every lake build has the Lean kernel check that no sequence of HTTP requests lets an authenticated principal read, modify, delete, or grant access to data beyond its legitimate permissions. You never have to write Lean.

Nyxis is under active development. Read ASSUMPTIONS.md for the scope of the guarantee and the assumptions trusted outside the proof before using it in production.

Highlights

• Cedar as the single source of truth: the schema doubles as the table definition (entity type = table, attribute = column), and each action carries exactly one Nyxis-defined effect via @effect(...).
• Proven authorization safety: the main theorem is Nyxis.Runtime.authorization_safety; Test/Axioms.lean checks the axioms of every theorem. See docs/proofs.md for the catalog of theorems.
• Restricted handlers: handlers have type Nyxis.Handler and cannot perform IO or reach the database directly. nyxis_approved and nyxis_check_app bind the app to the approved sources and audit the application code at build time.
• Runtime on PostgreSQL (Supabase) and Supabase Auth: an HTTP server that verifies Supabase Auth JWTs (with JWKS fetching), CORS, transactional reads and writes, storage signing, background jobs, an outbox for email and external API calls.
• Used as a Lake package: require nyxis from "<path>"; dependencies are pinned and verified by SHA256 via scripts/prepare-dependencies.py.

Official samples

• examples/bulletin-board/: published and draft posts, Google OAuth login, and granting and revoking admin rights, with a Next.js frontend.
• 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).

Documentation

README and ASSUMPTIONS are available in English and Japanese; the other documents under docs/ are currently in Japanese.