ZIL 是一种小型关系语言，用于描述命名对象、它们之间的关系以及推导额外关系的规则。一个关系有三个部分：主体 ── 关系 ──▶ 对象。例如：lean.Parser.parse ── implements ──▶ requirement.parseInput。ZIL 在 Lean 4 内部实现了这个模型。Lean 检查定义、可执行程序、定理陈述和证明。ZIL 记录这些经过检查的声明与需求、文档、测试、任务、依赖关系和项目其他部分之间的关系。同一项目映射可以回答诸如：哪个声明实现了这个需求？哪个定理验证了这个组件？哪些模块依赖于这个声明？哪个任务在等待这个结果？哪个声明在这个更改后需要审核？开发者、审核工具、持续集成、文档工具和 AI 助手可以查询相同的存储关系。关系元组：从 Zanzibar 到 ZIL。ZIL 的关系模型受到 Google Zanzibar 论文中描述的元组导向模型的影响：《Zanzibar：Google 的一致性全球授权系统》（USENIX ATC '19）。第 2.1 节将授权元组表示为：对象#关系@用户。表 1 给出了这些示例：doc:readme#owner@10，group:eng#member@11，doc:readme#viewer@group:eng#member，doc:readme#parent@folder:A。他们描述了四种有用的关系模式：用户 10 是 doc:readme 的所有者；用户 11 是 group:eng 的成员；group:eng 的成员是 doc:readme 的查看者；doc:readme 位于 folder:A。第三个元组使用用户集：group:eng#member。该用户集命名了与 group:eng 通过成员相关的所有人。因此，一个元组可以引用另一个关系，支持组成员资格和继承的访问权限。独立的 ZIL 可以表达相同的元组形状的事实：doc:readme#owner@user:10，group:eng#member@user:11，doc:readme#viewer@group:eng#member，doc:readme#parent@folder:A。原生 ZIL Lean 语法使用 Lean 名称表示关系：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 使用关系元组描述授权数据。ZIL 使用相同的紧凑关系构建块用于授权模型和更广泛的项目关系：文档 ───── 观看者 ──────▶ 组；声明 ── 实现 ──▶ 需求；定理 ────── 验证 ────▶ 组件；模块 ─────── 依赖于 ────▶ 模块；任务 ───────── 被 ────▶ 问题；声明 ──────── 支持 ──▶ 文档。Datalog 风格的规则。表 1 提示关系数据。规则描述如何从该数据推导出额外的关系。ZIL 使用 Horn 规则，这是 Datalog 系统常用的规则形式。例如：当一个组可以查看一个文档且一个用户属于该组时，该用户可以查看该文档。在 ZIL Lean 中：zil_theorem_rule groupViewer {document group user : Zil.Node} (hViewer : document ⟶[viewer] group) (hMember : group ⟶[member] user) : document ⟶[viewer] user。给定：doc.readme ─────────── 观看者 ──▶ group.engineering；group.engineering ──── 成员 ──▶ user.u11。重复的规则评估增加：doc.readme ── 观看者 ──▶ user.u11。相同的规则结构可以推导项目关系，如需求覆盖和变更影响。项目示例考虑一个包含解析器、规范化过程和关于规范化输出的定理的项目：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)。这些事实形成一个关系图：requirement.parseInput ▲ │ 实现 lean.Parser.parse ▲ │ 依赖于 lean.Normalize.normalize ▲ │ 验证 lean.Normalize.normalized_sound。Lean 检查解析器、规范化程序、定理陈述和证明。ZIL 存储它们的项目角色和连接。查询可以询问：哪个声明实现了 requirement.parseInput；哪些组件依赖于解析器；哪些转换具有验证定理；在更改后哪些下游声明应被审查。规则推导项目关系。规则可以推导直接变更影响：zil_theorem_rule propagateImpact {changed dependent : Zil.Node} (hDepends : dependent ⟶[dependsOn] changed) : changed ⟶[affects] dependent。从解析器依赖，发起引擎添加：lean.Parser.parse ── 影响 ──▶ lean.Normalize.normalize。第二个规则通过多个层级继续关系：zil_theorem_rule propagateTransitiveImpact {source middle target : Zil.Node} (hFirst : source ⟶[affects] middle) (hSecond : target ⟶[dependsOn] middle) : source ⟶[affects] target。局部依赖事实可以支持整个库的审查查询。Lean 和 ZIL 在一个项目中。Lean 验证术语、类型、定义、计算、定理陈述和证明。ZIL 存储有关目的的关系，