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

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]