ZIL Lean: реляционный слой для связывания кода, требований и доказательств в Lean 4

В мире формальной верификации и сложной логики часто возникает проблема «разрыва» между кодом, его требованиями и доказательствами корректности. ZIL Lean предлагает решение в виде компактного реляционного языка, встроенного непосредственно в Lean 4. В отличие от стандартных комментариев или внешних трекеров задач, ZIL фиксирует отношения между сущностями проекта как данные, которые можно проверять, выводить новые факты и использовать в автоматизированных пайплайнах.

Архитектура инструмента опирается на модель кортежей, описанную в документе Google Zanzibar. Базовая единица — отношение «субъект — связь — объект». Например, можно зафиксировать, что конкретная функция реализует определённое требование, а теорема валидирует модуль. Такая структура позволяет выражать не только прямые зависимости, но и сложные иерархии, такие как членство в группах или наследование прав доступа, что делает модель универсальной для описания ролей в автоматизированных рабочих процессах.

Ключевой особенностью ZIL является использование правил Horn-логики (Datalog) для вывода новых отношений. Если известно, что группа имеет право просматривать документ, а пользователь входит в эту группу, движок автоматически выводит, что пользователь может просматривать документ. Аналогичная логика применяется к анализу влияния изменений: если модуль A зависит от B, а C зависит от A, система строит цепочку зависимостей, помогая разработчикам понимать, какие части кода потребуют пересмотра после изменения базовой функции.

Для задач, выходящих за рамки стандартного Datalog, проект предлагает модуль Zil.Horn. Он поддерживает более сложную логику программирования, включая вложенные конструкторы, рекурсивные предикаты и SLD-разрешение с бэктрекингом. Это позволяет использовать ZIL для проверки структурных свойств контрактов формализации, например, подтверждения того, что все заявленные требования имеют соответствующие доказательства или реализации в коде.

Инструмент обеспечивает прозрачность вычислений. Каждое выведенное отношение сопровождается «аудируемым следом»: указанием исходных фактов, применённого правила и связывания переменных. Это критически важно для отладки сложных логических цепочек и для доверия к результатам, полученным ИИ-ассистентами или CI-системами. Разработчики могут использовать встроенные линтеры для проверки покрытия требований и целостности графа зависимостей.

ZIL Lean интегрируется с экосистемой через стандартные механизмы Lean, такие как Lake и расширения окружения. Данные можно экспортировать в форматы Soufflé Datalog или Prolog, что позволяет использовать внешние аналитические инструменты. Проект фиксирует версию Lean 4.31.0 и предоставляет набор примеров, демонстрирующих от простых фактов до сложных многошаговых запросов по графу проекта.

Таким образом, ZIL Lean превращает разрозненные элементы кодовой базы в связный граф знаний. Это позволяет автоматизировать ответы на вопросы о покрытии требований, зависимостях модулей и статусе задач, создавая единый источник истины для людей и машинных агентов.