Show HN: Lean4 Datalog DSL Based on Google Zanzibar for AI Projects

A new open-source Lean 4 Datalog DSL called ZIL, inspired by Google's Zanzibar authorization system, allows developers to model relationships between code, requirements, tests, and tasks using compact relational tuples and Horn rules. ZIL records how Lean declarations relate to project artifacts, enabling queries such as which declaration implements a requirement or which modules depend on a declaration, and supports AI assistants, CI, and documentation tools. The project's relation model mirrors Zanzibar's tuple-oriented approach, with examples showing how rules can derive additional relationships like transitive viewer access or requirement coverage.

ZIL is a small relational language for describing named objects, the relationships between them, and rules that derive additional relationships. A relation has three parts: subject ── relation ──▶ object For example: lean.Parser.parse ── implements ──▶ requirement.parseInput ZIL Lean implements this model inside Lean 4. Lean checks definitions, executable programs, theorem statements, and proofs. ZIL records how those checked declarations relate to requirements, documents, tests, tasks, dependencies, and other parts of a project. The same project map can answer questions such as: which declaration implements this requirement? which theorem validates this component? which modules depend on this declaration? which task is waiting for this result? which declarations should be reviewed after this change? Developers, review tools, CI, documentation tools, and AI assistants can query the same stored relationships. ZIL's relation model is influenced by the tuple-oriented model described in Google's Zanzibar paper: Zanzibar: Google's Consistent, Global Authorization System USENIX ATC '19 https://storage.googleapis.com/gweb-research2023-media/pubtools/5068.pdf Section 2.1 represents an authorization tuple as: object relation@user Table 1 gives these examples: doc:readme owner@10 group:eng member@11 doc:readme viewer@group:eng member doc:readme parent@folder:A ... They describe four useful relation patterns: user 10 is an owner of doc:readme user 11 is a member of group:eng members of group:eng are viewers of doc:readme doc:readme is in folder:A The third tuple uses the userset: group:eng member This userset names everyone related to group:eng through member . A tuple can therefore refer to another relation, supporting group membership and inherited access. Standalone ZIL can express the same tuple-shaped facts: doc:readme owner@user:10. group:eng member@user:11. doc:readme viewer@group:eng member. doc:readme parent@folder:A. Native ZIL Lean syntax represents the relations with Lean names: python import Zil zil fact node doc.readme ⟶ owner node user.u10 zil fact node group.engineering ⟶ member node user.u11 zil fact node doc.readme ⟶ viewer node group.engineering Zanzibar uses relation tuples to describe authorization data. ZIL uses the same compact relational building blocks for authorization models and for wider project relationships: document ───── viewer ──────▶ group declaration ── implements ──▶ requirement theorem ────── validates ────▶ component module ─────── dependsOn ────▶ module task ───────── blockedBy ────▶ issue claim ──────── supportedBy ──▶ document Table 1 presents relation data. Rules describe how additional relations follow from that data. ZIL uses Horn rules, the rule form commonly used by Datalog systems. For example: when a group can view a document and a user belongs to that group, the user can view the document In ZIL Lean: zil theorem rule groupViewer {document group user : Zil.Node} hViewer : document ⟶ viewer group hMember : group ⟶ member user : document ⟶ viewer user Given: doc.readme ─────────── viewer ──▶ group.engineering group.engineering ──── member ──▶ user.u11 repeated rule evaluation adds: doc.readme ── viewer ──▶ user.u11 The same rule structure can derive project relationships, such as requirement coverage and change impact. Consider a project containing a parser, a normalization pass, and a theorem about normalized output: python import Zil zil fact node lean.Parser.parse ⟶ implements node requirement.parseInput zil fact node lean.Normalize.normalize ⟶ dependsOn node lean.Parser.parse zil fact node lean.Normalize.normalized sound ⟶ validates node lean.Normalize.normalize These facts form a relationship map: requirement.parseInput ▲ │ implements lean.Parser.parse ▲ │ dependsOn lean.Normalize.normalize ▲ │ validates lean.Normalize.normalized sound Lean checks the parser, normalizer, theorem statement, and proof. ZIL stores their project roles and connections. A query can ask: - which declaration implements requirement.parseInput ; - which components depend on the parser; - which transformations have a validation theorem; - which downstream declarations should be reviewed after a change. A rule can derive direct change impact: zil theorem rule propagateImpact {changed dependent : Zil.Node} hDepends : dependent ⟶ dependsOn changed : changed ⟶ affects dependent From the parser dependency, the engine adds: lean.Parser.parse ── affects ──▶ lean.Normalize.normalize A second rule continues the relationship through several levels: zil theorem rule propagateTransitiveImpact {source middle target : Zil.Node} hFirst : source ⟶ affects middle hSecond : target ⟶ dependsOn middle : source ⟶ affects target Local dependency facts can therefore support a repository-wide review query. Lean verifies terms, types, definitions, computation, theorem statements, and proofs. ZIL stores relationships concerning purpose, coverage, dependencies, evidence, tasks, and review work across the repository. Together they support questions such as: - Which declaration implements a requirement? - Which theorem validates a transformation? - Which modules depend on a changed declaration? - Which claims have supporting documents? - Which work items are waiting for a result? - Which advertised capabilities have implementation links? - Which facts and rules produced an inferred relationship? - Which project assumptions changed since the previous work session? These relationships can connect Lean declarations to requirements, documents, issues, tests, tools, and external sources across many modules. ZIL uses four primary structures: nodes identify declarations, requirements, claims, tests, files, tasks, users, groups, or other objects; relations connect two terms; rules derive relations from existing relations; queries return matching terms and variable bindings. Nodes use stable names: lean.Parser.parse lean.Normalize.normalized sound requirement.parseInput component.normalizer issue.missingTerminationProof document.design.section4 assistant.formalization The repository pins Lean to: leanprover/lean4:v4.31.0 Build the package and run the Lean tests: lake build lake exe zilLeanTests Progressive native examples are under examples/lean/ : lake env lean examples/lean/01 FactsAndRelations.lean lake env lean examples/lean/02 TheoremShapedRule.lean lake env lean examples/lean/03 TypedRule.lean lake env lean examples/lean/04 MultiStepQuery.lean lake build KnowledgeBase lake env lean examples/lean/05 ImportedKnowledge.lean lake env lean examples/lean/06 ProjectVerificationArc.lean All documented example groups are also runnable through the Makefile: make examples lean, native, integration, and legacy groups make examples GROUP=lean one group; report in .zil/examples-reports/ Register a fact: zil fact node lean.Parser.parse ⟶ implements node requirement.parseInput Declare a theorem-shaped rule: zil theorem rule implementationCoversRequirement {declaration requirement : Zil.Node} hImplements : declaration ⟶ implements requirement : requirement ⟶ coveredBy declaration The block form expresses the same rule: zil rule implementationCoversRequirement where variables declaration requirement premises declaration ⟶ implements requirement conclusion requirement ⟶ coveredBy declaration Both forms produce the standard Zil.Rule value used by the engine and tools. A query can retrieve the implementation covering a requirement: private def coverageQuery : Zil.Query := { name := implementationForRequirement variables := declaration select := declaration premises := .mk' .ground requirement.parseInput zil.coveredBy .variable declaration } The engine binds variables, matches several premises, removes repeated results, and applies rules until the result set becomes stable within the configured bound. A relation schema records the expected source and target types: implements : declaration → requirement validates : theorem → component dependsOn : declaration → declaration blockedBy : task → requirement supportedBy : claim → evidence member : group → user viewer : document → user-or-group A typed rule declares the type of each variable: zil typed rule typedCoverage using Zil.Profile.research where variables declaration : declaration requirement : requirement premises declaration ⟶ implements requirement conclusion requirement ⟶ coveredBy declaration guard typedCoverage.valid The schema reports category mistakes while keeping the underlying rule available for messages and tools. ZIL stores selected project facts with the source code. Developers, reviewers, build tools, documentation tools, issue trackers, and AI assistants can use the same map. file.Parser.lean ── responsibleFor ──▶ requirement.parseInput lean.Parser.parse ── implements ─────▶ requirement.parseInput A developer or assistant can inspect why a file exists and which requirement its declarations serve before editing it. requirement.totalParser ── blockedBy ──▶ issue.missingTerminationProof issue.missingTerminationProof ── assignedTo ──▶ task.proveTermination Queries can find blocked requirements, tasks awaiting an owner, and capabilities awaiting an implementation link. lean.Normalize.normalize ── dependsOn ──▶ lean.Parser.parse lean.Codegen.emit ───────── dependsOn ──▶ lean.Normalize.normalize Impact rules return the downstream components that require review when lean.Parser.parse changes. zil checkpoint beforeParserRefactor zil check mutation token Change checks compare graph revisions, contracts, stated goals, and rollback checkpoints before automated work continues. Each inferred relation can record: input project facts rule name variable bindings trust level input relation identifiers This gives developers and tools a step-by-step explanation of how the engine reached a result. ZILX/1 snapshots and ZILD/1 deltas allow separate tools to exchange the same project map. One tool may inspect requirements, another implement code, another verify proofs, and another review impact while sharing stable relation names and revision numbers. Authorization-style relations can also describe roles in an automated workflow: repo.zilLean ── editor ─────▶ group.implementers group.implementers ─ member ▶ assistant.codegen repo.zilLean ── reviewer ───▶ assistant.verifier The tuple model therefore supports project context and role-based access to project operations. Facts, rules, schemas, contracts, checkpoints, declaration links, and proof-backed rules use Lean environment extensions. Compiled .olean imports restore registered entries and collapse repeated diamond imports into one relation. The coverage linter evaluates the stored and inferred relations: zil lint zil lint A formalization contract can record required declarations, required relations, advertised scope, completion state, and revision history: zil register contract contract zil contract check zil contract check Contracts give maintainers and tools a shared description of the expected result of a task or file. ZIL records three trust levels: asserted graphDerived certified asserted marks a directly registered project fact; graphDerived marks an inferred relation; certified associates a rule with a Lean proposition and proof term. private theorem certificate : True := True.intro private def certifiedRule : Zil.Trust.CertifiedRule := .mkChecked graphRule True certificate zil register certified rule certifiedRule Lean checks the proposition and proof term. ZIL records how the checked declaration participates in the project map. For inferred relationships, the explanation data records the project fact, source, rule name, variable binding, trust level, and input relation identifiers. Developers and tools can use that data to show how a result was reached. The native zil executable reads .zc models and ZILR/1 revision logs: bin/zil expand examples/native-cli/formalization-claims.zc - bin/zil query-ci examples/native-cli/formalization-claims.zc bin/zil revision-summary examples/revision/release.zilr bin/zil snapshot examples/revision/release.zilr 2 - Supported operations include compile , expand , trace , query-ci , explain-query , explain-authorization , dependency-graph , impact , authorize , revision-summary , snapshot , and causal-check bin/zil --help lists them all . See examples/native-cli/README.md for the walkthrough. Relations and rules have deterministic text codecs: Zil.Codec.encodeRelation Zil.Codec.decodeRelation Zil.Codec.encodeRule Zil.Codec.decodeRule ZILX/1 stores revisioned snapshots. ZILD/1 stores incremental updates with base and target revisions, fact changes, rule changes, and schema changes. Facts and rules can be exported to Soufflé Datalog or Prolog: zil export souffle zil export prolog These interfaces let external analysis tools and assistants consume the same relational state used by the Lean implementation. ZIL Lean can support: - Zanzibar-style authorization and group-membership models; - maps connecting informal claims to Lean declarations; - requirement-to-implementation tracking; - theorem and component dependency analysis; - change-impact queries across modules; - evidence and source tracking; - repository coverage checks; - explicit task contracts for people and tools; - AI assistants continuing work across sessions with revision and checkpoint checks; - step-by-step explanations for inferred project relationships; - exchange of relation data with Datalog and Prolog tools. The repository also contains the standalone ZIL syntax and Clojure/DataScript runtime. It supports .zc files, macros, import/export tools, embedded annotations, and adapters. clojure -M -m zil.cli examples/it-infra-minimal.zc The standard exchange layer connects that runtime with the native Lean representation. Zil/ native Lean library Zil/Engine/ Horn-rule evaluation and relationship explanations Zil/Trust/ proof-backed rules Zil/Exchange/ snapshots and deltas examples/lean/ progressive native examples examples/native-cli/ CLI snapshot example src/zil/ Clojure runtime and tools spec/ language and runtime specifications Expected repository validation: lake build lake exe zilLeanTests clojure -M:test The Lean toolchain is pinned to leanprover/lean4:v4.31.0 .