Что это
Guardians - открытая Python-библиотека, реализующая идеи статьи Erik Meijer «Guardians of the Agents: Formal Verification of AI Workflows» (Communications of the ACM, январь 2026). Идея в том, что prompt injection в агентных системах устроен так же, как SQL injection: код и данные не разделены. Вместо того чтобы агент вызывал инструменты по одному и решал следующий шаг по ответу, LLM сразу строит структурированный план с символическими ссылками вместо реальных данных, а статический верификатор проверяет этот план по политике безопасности до запуска любых инструментов. Проверка включает три независимых механизма: taint-анализ (не течут ли данные из источника в запрещённую точку), автоматы безопасности (не приводит ли последовательность вызовов инструментов в аварийное состояние) и доказательство теорем через Z3 (выполняются ли предусловия и условия сохранения). Во время выполнения дополнительно проверяются allowlist инструментов, пред- и постусловия, состояния автомата и бюджеты вызовов.
Для участника клуба, который собирает агентов и автоматизации на n8n, кастомных пайплайнах или своих LLM-агентах, Guardians полезен как референс архитектуры защиты от prompt injection: показывает, как декларативно описать инструменты и политики через GuardedAgent (декораторы для taint-меток, правила deny/allow по доменам и т.п.) и получить проверяемую гарантию, что агент не выполнит вредоносный план из письма или документа. Это не готовый сервис с интерфейсом, а библиотека и референсная реализация для тех, кто пишет собственный агентный код на Python и хочет добавить слой формальной проверки безопасности перед выполнением действий (отправка писем, изменение файлов и т.д.).
Возможности
- Статический верификатор проверяет план агента до выполнения любого инструмента
- Taint-анализ отслеживает поток данных от источников к запрещённым точкам (sinks)
- Автоматы безопасности контролируют допустимую последовательность вызовов инструментов
- Верификация через Z3 theorem prover проверяет предусловия и условия сохранения плана
- LLM строит план с символическими ссылками (placeholders) вместо реальных данных, разделяя код и данные
- GuardedAgent - высокоуровневый API с декораторами для описания инструментов, taint-меток и политик deny/allow
- Runtime-проверки во время исполнения: allowlist инструментов, пред/постусловия, состояния автомата, бюджеты вызовов
- Минимум зависимостей (pydantic, z3-solver), Python 3.11+, около 1900 строк кода и 100 тестов
Цена: Открытый исходный код на GitHub (MIT-подобная модель распространения), без коммерческих тарифов; единственные возможные расходы - оплата LLM API, если подключать опциональный модуль litellm для планирования
