nyxfoundation/nyxis is a Lean backend framework that checks access permissions according to Cedar schemas and policies. Developers write the Cedar schemas and policies, while request handling uses Supabase Auth and PostgreSQL. The latest release is v0.1.9. The provided material does not record what changed in this version, so the specific changes cannot be confirmed.
The core of the design is to guarantee the authorization behavior under Cedar policies through formal proofs. A formal proof is a way of checking, by mathematical logic, whether a given rule holds. According to the README, the type of the request handler is restricted so that it can only call the permission-checking layer, and the build process runs the proofs and application checks. The core implementation and two example backends are organized as Lean projects, and documentation on proofs, dependencies, and connections is provided as well. The repository is MIT licensed.
However, the README states that the project is under development and points to separate documentation for the actual scope of the guarantees and the assumptions outside the proofs. Therefore, claims about permission guarantees should not be read as extending to the safety of the system as a whole. The current material does not confirm the v0.1.9 changelog either, so the boundaries of the guarantees and the differences between versions must be checked through the relevant documentation.