ZIL is a small relational language for describing named objects, the relationships between them, and rules that derive additional relationships. Inspired by Google's Zanzibar tuple‑based authorization model, ZIL lets you represent a knowledge base that can be stored under Git and queried without heavyweight external infrastructure. The core model consists of nodes (identifying declarations, requirements, claims, tests, files, tasks, users, groups, etc.), relations connecting two nodes, rules that derive new relations from existing ones, and queries that return matching terms and variable bindings.

In the Lean 4 implementation, ZIL facts are expressed with Lean names, e.g., `zil_factnode(lean.Parser.parse)⟶[implements]node(requirement.parse Input)`. Rules are Horn‑style, such as deriving that a user can view a document when they belong to a group that has view permission. These rules enable project‑wide queries like “which declaration implements this requirement?” or “which modules depend on a changed declaration?” and support change‑impact analysis through transitive propagation.

Together, Lean’s verification of definitions, proofs, and computations and ZIL’s storage of purpose, coverage, dependencies, evidence, tasks, and review work answer questions about requirement validation, transformation verification, dependency tracking, and pending work items. Relationships can link Lean declarations to requirements, documents, issues, tests, tools, and external sources across many modules, benefiting developers, review tools, CI pipelines, documentation generators, and AI assistants.

The repository pins Lean to a specific version and provides progressive examples under `examples/lean/`. Users can build with `lake build`, run Lean tests with `lake test`, and execute example files via `lake env lean examples/lean/01_Facts_And_Relations.lean` through `06_Project_Verification_Arc.lean`. All example groups are also runnable via the Makefile (`make examples`).