ZIL Lean: DSL для Lean 4 по модели Google Zanzibar связывает код с требованиями
На Hacker News (раздел Show HN) опубликован проект ZIL Lean, небольшой реляционный DSL (предметно-ориентированный язык), встроенный в язык доказательств Lean 4. Автор описывает его как применение модели данных из статьи Google о системе авторизации Zanzibar (Zanzibar: Google's Consistent, Global Authorization System, USENIX ATC '19) не к разграничению доступа, а к описанию связей внутри программного проекта.
В основе лежит формат кортежей из статьи Zanzibar: объект#отношение@пользователь (например, doc:readme#owner@10, «пользователь 10 является владельцем doc:readme», или doc:readme#viewer@group:eng#member, «участники группы eng являются читателями doc:readme»). ZIL переносит этот же формат на произвольные проектные сущности: требование ⟵ implements ⟵ объявление, компонент ⟵ validates ⟵ теорема, модуль ⟵ dependsOn ⟵ модуль, задача ⟵ blockedBy ⟵ issue. Факты записываются прямо в коде через zil_fact, а дополнительные связи выводятся правилами Хорна (стандартная форма правил в системах Datalog) через zil_theorem_rule, например, правило «если группа видит документ, а пользователь входит в группу, то пользователь тоже видит документ» или правило распространения влияния изменений («если B зависит от A, то изменение A влияет на B», с транзитивным продолжением через несколько уровней зависимостей).
Поскольку всё построено внутри Lean 4, который проверяет определения, программы, формулировки теорем и доказательства, ZIL размечает три уровня доверия к связи: asserted (факт зарегистрирован вручную), graphDerived (выведен правилом) и certified (правило подкреплено доказанной леановской теоремой). Инструмент поддерживает типизированные схемы отношений (например, implements: declaration → requirement), запросы к графу связей (какое объявление реализует требование, какие модули зависят от изменённого объявления, какие требования заблокированы), линтер покрытия (#zil_lint), формализованные «контракты» со списком обязательных связей и ревизией, а также точки отката (checkpoint) и проверку мутаций (#zil_check_mutation), по замыслу автора, это должно позволять безопасно проводить автоматизированную работу над кодом, в том числе силами ИИ-ассистентов, которые могут читать и обновлять тот же граф связей, что и разработчики, CI и инструменты документации.
Проект собирается через lake build и закреплён на версии leanprover/lean4:v4.31.0; в репозитории есть набор примеров (от базовых фактов и правил до многошаговых запросов) и Makefile для их запуска по группам.
Ключевые факты
- ZIL Lean, DSL для Lean 4, переносящий модель авторизационных кортежей Google Zanzibar (
объект#отношение@пользователь) на связи внутри проекта: требования, тесты, задачи, зависимости кода. - Связи задаются фактами (
zil_fact) и выводятся правилами Хорна (zil_theorem_rule/zil_rule), включая транзитивный анализ влияния изменений по цепочке зависимостей. - Каждая выведенная связь получает один из трёх уровней доверия:
asserted(внесена вручную),graphDerived(выведена правилом),certified(подкреплена доказанной Lean-теоремой). - Инструментарий включает типизированные схемы отношений, запросы к графу, линтер покрытия, формальные «контракты» на обязательные связи и точки отката для проверки автоматических изменений (в том числе ИИ-ассистентами).
- Проект собирается через
lake build, закреплён на Lean 4 версии v4.31.0; репозиторий содержит примеры и Makefile для их запуска.
Почему это важно
ZIL Lean интересен не сам по себе как ещё один DSL, а тем, что берёт модель отношений из промышленной системы авторизации (Zanzibar, на которой построен, в частности, доступ в Google Drive и YouTube) и переиспользует её для другой задачи, трассировки требований и связей внутри кодовой базы. Поскольку язык встроен в Lean 4, часть связей можно не просто задекларировать, а формально подтвердить доказанной теоремой (уровень доверия certified), это редкое сочетание системы отслеживания требований с математической проверкой.
Кому это важно
В первую очередь, разработчикам на Lean 4 и командам, которые занимаются формальной верификацией и хотят автоматически отслеживать, какой код реализует какое требование, какие модули затронет правка и какие задачи заблокированы. Автор явно упоминает и ИИ-ассистентов как участников, инструмент задуман так, чтобы модель, ревьюер-человек, CI и документация читали один и тот же граф связей и могли проверять мутации кода перед тем, как их принять.
Как это применить
Проект открыт на GitHub (jagg-ix/zil-lean), собирается командой lake build при закреплённой версии Lean leanprover/lean4:v4.31.0; тесты запускаются через lake exe zilLeanTests. В репозитории есть прогрессивная серия примеров (от базовых фактов и правил до многошаговых запросов и импортированной базы знаний) и Makefile для запуска групп примеров (make examples GROUP=lean). Условия лицензирования и коммерческого использования в тексте источника не указаны.
Можно ли доверять
Источник, собственное описание автора в README проекта на GitHub, независимого подтверждения заявленной функциональности в материале нет. На момент публикации на Hacker News пост совсем свежий (около двух часов), набрал всего 8 очков и не получил ни одного комментария, то есть сообщество ещё не успело оценить или раскритиковать подход. Сам репозиторий и код по ссылке существуют, структура примеров и API выглядит проработанной, но это не заменяет независимой проверки.
Риски и подводные камни
Аудитория Lean 4 сама по себе узкая, что ограничивает потенциальный круг пользователей такого DSL. Отсутствие обсуждения на HN не позволяет судить о реальной зрелости и надёжности инструмента. Уровни доверия к связям (asserted, graphDerived, certified) во многом опираются на то, что разработчик сам корректно расставил факты и правила, ошибка на этом уровне тихо распространится по графу выводов. Дополнительный слой Datalog-подобных правил поверх и без того сложного языка доказательств Lean повышает порог входа для команд, которые ещё не используют Lean 4 в проекте.