ZIL es un lenguaje relacional compacto, implementado dentro de Lean 4, que permite describir objetos con nombre, las relaciones entre ellos y reglas que derivan relaciones adicionales a partir de hechos existentes. Su modelo se inspira en el enfoque de tuplas empleado por el sistema Zanzibar de Google, donde una relación se expresa como sujeto–relación–objeto y puede incluir usuarios (usersets) para representar pertenencia a grupos o accesos heredados.
En el contexto de un proyecto de software, ZIL registra cómo las declaraciones verificadas por Lean —definiciones, programas ejecutables, teoremas y pruebas— se vinculan con requisitos, documentos, pruebas, tareas, dependencias y otros componentes. De este modo, un mismo mapa relacional permite responder preguntas como qué declaración implementa un requisito, qué teorema valida un componente, qué módulos dependen de un cambio, qué tareas esperan un resultado o qué elementos deben revisarse tras una modificación.
El lenguaje articula sus capacidades en cuatro estructuras: nodos (que identifican declaraciones, requisitos, tests, archivos, usuarios, etc.), relaciones que conectan dos términos, reglas al estilo Datalog que derivan nuevas relaciones y consultas que devuelven coincidencias. Las reglas, escritas con sintaxis nativa de Lean (zil_theorem_rule), pueden propagar impactos directos o transitivos a través de cadenas de dependencias, permitiendo análisis de cobertura de requisitos y de alcance de cambios en todo el repositorio.
El repositorio fija Lean a la versión v4.31.0 y ofrece ejemplos ejecutables con Lake para ilustrar hechos, reglas con forma de teorema, reglas tipadas, consultas multietapa, bases de conocimiento importadas y arcos de verificación de proyecto. Está dirigido a desarrolladores, herramientas de revisión, sistemas de CI, herramientas de documentación y asistentes de IA que necesiten consultar el mismo grafo de relaciones del proyecto.