2026-07-29 02:22 UTCIn-site rewrite5 min readUpdated: 2026-07-29 02:58 UTC

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

ZIL is a relational language for Lean 4 that models relationships between project entities (declarations, requirements, etc.) using Datalog-like rules inspired by Google Zanzibar.

SourceHacker News AIAuthor: kbradero

Notifications You must be signed in to change notification settings

Fork 0

Star 1

BranchesTags

Open more actions menu

Folders and files

NameName

Last commit message

Last commit date

Latest commit

History

27 Commits

Zil

architecture

bin

config

examples

extensions/reference

formal/dmetavm

lib

libsets

notes

profiles

projects

scripts

spec

src/zil

test

tools

.dockerignore

.gitignore

Dockerfile.test

INSTALL-BUNDLES.md

INSTALLING.md

Makefile

PUBLIC-CONTENT-POLICY.md

README.md

TESTING.md

Zil.lean

build.clj

compose.test.yml

deps.edn

lake-manifest.json

lakefile.lean

lean-toolchain

legacy-retirement.edn

port-gate.edn

Repository files navigation

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.

Relation tuples: from Zanzibar to ZIL

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)

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:

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

Datalog-style rules

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.

A project example

Consider a project containing a parser, a normalization pass, and a theorem about normalized output:

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.

Rules derive project relationships

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 and ZIL in one project

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.

Core model

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

Quick start

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/

Facts, rules, and queries

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.

Relation schemas

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.

Shared project maps for people 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.

Continue work from a previous session

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.

Find work that is waiting

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.

Calculate change impact

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.

Check long-running changes

zil_checkpoint beforeParserRefactor #zil_check_mutation token

Change checks compare graph revisions, contracts, stated goals, and rollback checkpoints before automated work continues.

Explain inferred relationships

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.

Share context between tools

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

[truncated for AI cost control]