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)
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
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:
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
.