Implementing Zanzibar in Lean4: A Formally Verified Permission Engine for AI Projects

Introduction: When Permission Systems Meet Formal Verification

On Hacker News's Show HN section, an ambitious open-source project caught the tech community's attention — a Datalog DSL (Domain-Specific Language) built on the Google Zanzibar model, implemented in Lean4, specifically designed for permission management in AI projects.

What makes this project unique is that it sits at the intersection of two cutting-edge technologies: on one side, Zanzibar — Google's authorization system architecture proven in large-scale production environments; on the other, Lean4 — a theorem prover renowned for its rigorous mathematical proofs. Combining the two means developers can not only leverage a flexible relation-based permission model but also use formal verification to guarantee the correctness of permission logic.

Google Zanzibar: The Gold Standard of Permission Systems

What Problem Does Zanzibar Solve?

Google Zanzibar was originally designed as a unified authorization system to support massive products like YouTube, Google Drive, and Google Photos. It processes trillions of access control list (ACL) entries for billions of users daily, completing permission checks with extremely low latency.

Google officially published the design details of this system in 2019 through the paper Zanzibar: Google's Consistent, Global Authorization System. The system has been running internally at Google since 2016, uniformly managing authorization logic across hundreds of products. Its core design includes: globally consistent storage based on the Spanner database, causal consistency semantics achieved through Zookies (opaque tokens), and a distributed evaluation engine supporting millions of permission checks per second. After the Zanzibar paper was published, it quickly spawned multiple open-source implementations, including SpiceDB by the Authzed team, Keto by the Ory team, and OpenFGA incubated by the CNCF. Together, these projects have driven ReBAC (Relationship-Based Access Control) to become the dominant paradigm in cloud-native authorization.

Zanzibar's core idea is Relation Tuples. Rather than using traditional RBAC (Role-Based) or ABAC (Attribute-Based) models, it uses triples of the form object#relation@user to describe permission relationships. For example, document:readme#viewer@user:alice means Alice has viewing permission on the readme document.

The elegance of this model lies in the fact that complex permission logic (such as "editors of a folder automatically become editors of all files within it") can be expressed through composition and inheritance of relations, without hard-coding.

Why Use Datalog to Express Zanzibar Permission Logic?

Datalog, as a declarative logic query language, is naturally suited for expressing relation-reasoning-based permission systems like Zanzibar. The transitivity, inheritance, and composition of permissions are essentially a series of recursive logical derivation rules — and that's precisely Datalog's strength.

Datalog originated from the database research community in the 1980s. It is a syntactic subset of Prolog but with stronger computational predictability. Unlike Prolog, Datalog guarantees that all queries will terminate (because it prohibits function symbols, thereby ensuring the finiteness of the derivation process). A Datalog program consists of facts and rules: facts describe known base relations, and rules define how to derive new relations from existing ones. Its core evaluation strategy is fixed-point computation — repeatedly applying rules until no new facts are produced. In recent years, Datalog has gained widespread adoption in program analysis (e.g., Soufflé for pointer analysis), security policy specification (e.g., the underlying logic of AWS's Cedar language), and knowledge graph reasoning.

Implementing Zanzibar in Datalog means developers can declare permission logic with concise rules while leaving complex relational derivation to the query engine to handle automatically. For example, a permission inheritance rule can be expressed as something like can_access(User, File) :- parent(Folder, File), can_access(User, Folder), and the system will automatically perform recursive derivation along the relation graph.

Lean4 Formal Verification: From Usable to Provable

Lean4 Is More Than a Programming Language

Lean4 is a tool that serves the dual role of a functional programming language and an interactive theorem prover. It can both write high-performance real-world programs and conduct rigorous mathematical proofs about program properties.

Lean4 was developed primarily by Leonardo de Moura at Microsoft Research and is the fourth major version of the Lean theorem prover, released in 2021. Unlike previous generations, Lean4 was completely rewritten — it's not just a proof assistant but also a general-purpose pure functional programming language with efficient reference-counting memory management and the ability to compile to native code. Lean4's type system is based on the Calculus of Inductive Constructions and supports dependent types — meaning types can depend on values. This allows developers to encode program specifications at the type level, with the compiler enforcing that programs satisfy these specifications. Lean4's most famous recent application has been its use by mathematicians like Terence Tao to formalize mathematical theorem proofs, demonstrating the tool's powerful capabilities in rigorous reasoning.

Building the permission system's DSL on top of Lean4 brings a capability that traditional implementations can hardly match: the ability to formally verify the permission rules themselves. For example, you can prove that "any user not explicitly authorized can never gain access through rule combinations," or that "permission revocation will always cascade to all derived permissions."

The fundamental difference between formal verification and traditional software testing lies in coverage: testing can only verify a finite combination of inputs, while formal verification can prove that a program satisfies specific properties for all possible inputs. In permission systems, this distinction is especially critical — security vulnerabilities often hide in boundary conditions and the gaps between rule combinations, precisely where testing is most likely to miss. For instance, unexpected interaction effects between permission rules may cause certain paths to open unintentionally. Formal verification can prove "unreachability" — that is, mathematically proving certain undesirable states can never occur. However, the cost of formal verification is also significantly higher than testing: writing proofs is typically more time-consuming than writing the code itself and requires specialized skills.

A Permission Engine Tailored for AI Projects

This project explicitly positions its target scenario as AI projects, a point worth exploring in depth. With the proliferation of AI Agents, multi-agent systems, and RAG applications, permission management is becoming unprecedentedly complex:

• AI Agent delegated access: Agents need to access various resources on behalf of users, requiring clear permission boundaries
• Multi-model data isolation: Data access across multiple models and toolchains requires fine-grained control
• Sensitive data compliance: AI applications involving sensitive data have extremely high requirements for permission correctness

Permission management for AI Agents differs fundamentally from traditional human user permission management. In traditional systems, the permission subject is a human user whose behavior patterns are predictable with clear intent; AI Agents, however, may dynamically decide which resources to access based on context, with potentially long and unpredictable behavior chains. For example, an Agent using the ReAct pattern might autonomously decide to call multiple APIs and read multiple data sources while fulfilling a user request, forming a complex access graph. While emerging protocols like MCP (Model Context Protocol) define standard interfaces for tool invocation, fine-grained permission boundary management remains an open problem. Furthermore, in multi-Agent collaboration scenarios, permission delegation and trust propagation between Agents adds even more complexity — can one Agent sub-delegate some of its permissions to another Agent? Should such delegation have depth limits?

In these scenarios, a formally verifiable permission engine can provide additional security guarantees, preventing data leaks or privilege escalation caused by permission logic vulnerabilities. This is especially critical today as AI systems increasingly make autonomous decisions.

Advantages of the Technical Choices and Real-World Challenges

Core Advantages and Development Prospects

This technology stack combination reflects the author's pursuit of correctness first. Zanzibar provides an industrially validated architectural pattern, Datalog provides declarative expressiveness, and Lean4 caps it with correctness guarantees. For security-sensitive AI infrastructure, this is an attractive technical path.

From a technical architecture perspective, this layered design exhibits elegant separation of concerns: the Zanzibar model defines "how permissions should be modeled," Datalog defines "how permission rules are expressed and evaluated," and Lean4 answers "how to prove these rules are free of errors." Each layer operates in its area of greatest strength, combining to form a complete pipeline from modeling to expression to verification.

Real-World Challenges for Production Adoption

However, we must also soberly assess the challenges. Judging from the cold-start state of only 3 upvotes and 0 comments on Show HN, this project is still in a very early stage. Bringing academically flavored tools like Lean4 into production systems typically faces several practical hurdles:

• Steep learning curve: Formal verification in Lean4 requires a background in mathematics and type theory. Developers need to understand concepts like dependent types and inductive types, as well as master tactic proof writing — an entirely new knowledge domain for most engineers.
• Ecosystem immaturity: Compared to authorization systems implemented in Rust or Go (like SpiceDB, OpenFGA), the Lean4 ecosystem in the permissions space is virtually blank. The lack of ready-made database bindings, gRPC middleware, monitoring integrations, and other production-grade components means substantial infrastructure work must be built from scratch.
• Performance unproven: One of Zanzibar's core value propositions is extremely low latency (the paper reports p95 latency under 10 milliseconds). Whether a Lean4 implementation can achieve usable performance under real workloads remains to be proven. Although Lean4 can compile to native code, the performance of Datalog's fixed-point evaluation on large-scale relation graphs requires specialized optimization strategies such as semi-naive evaluation and index optimization.

Conclusion: The Value of Formal Verification in AI Security Infrastructure

Although this project is still in its infancy, the direction it represents — bringing formal verification into the security layer of AI infrastructure — holds forward-looking value. As AI systems increasingly take on critical decisions, ensuring "permission logic is free of vulnerabilities" will no longer be a nice-to-have but a hard requirement.

It's worth noting that formal methods have successful precedents in safety-critical systems: the seL4 microkernel proved through formal verification that its implementation is completely consistent with its specification, AWS uses TLA+ for model checking on core services like S3, and the CompCert compiler used Coq to prove semantic preservation during compilation. These cases demonstrate that when system security requirements are high enough, the investment in formal verification is worthwhile. AI permission systems are gradually crossing this threshold.

Regardless of whether this specific project ultimately matures into a production tool, the idea of using theorem provers as a safety net for AI permission systems deserves continued attention and exploration from the industry. It reminds us: while pursuing AI capabilities, building provably secure underlying infrastructure is equally important.