Hanzo публикует формальные доказательства для инфраструктуры ИИ-агентов

Сегодня мы открываем исходный код машинно проверенных формальных доказательств для инфраструктурного стека Hanzo AI. Это не тесты и не аудиты. Это математические гарантии, которые проверяет средство проверки типов Lean 4.

Что доказано

Безопасность агентов (6 доказательств)

• Границы возможностей: агент не может превысить выданные права
• Защита от эскалации: никакая последовательность действий не ведёт к неразрешённой возможности
• Вызов инструментов MCP: окно контекста сохраняется между вызовами
• Монотонность делегирования: переданные полномочия только сужаются и никогда не расширяются
• Порядок рабочего процесса: исполнение DAG соблюдает рёбра зависимостей
• Изоляция памяти: память агента только дополняется и ограничена релевантностью

Вычислительный слой (4 доказательства)

• Консенсус Proof of AI: целостность цепочки аттестации TEE и сходимость оценки качества при византийских отказах
• Конфиденциальные вычисления: изоляция анклава и свежесть аттестации
• Координация роя: справедливое распределение задач и сходимость балансировки нагрузки
• Корректность биллинга: измеренное использование никогда не завышает счёт

Шлюз и платформа (6 доказательств)

• Проверка токенов, справедливость ограничения частоты и корректность скользящего окна
• Безопасность отката blue-green-развёртывания и инвариант нулевого простоя
• Полнота цепочки поставок SBOM и монотонность учёта уязвимостей

KMS (1 доказательство)

• Соблюдение списка доступа к секретам: мастер-ключи никогда не пересекают границу HSM

В цифрах

• 17 файлов Lean 4, 0 sorry, 0 ошибок сборки
• 3 аксиомы, все моделируют аппаратные границы (изоляция TEE, периметр HSM, внешняя аутентификация)
• Lean 4.14.0 + Mathlib 4.14.0, зафиксированы и воспроизводимы
• Лицензия Apache 2.0

Зачем формальная верификация агентам ИИ

Агенты становятся самостоятельнее. Они пользуются инструментами, распоряжаются деньгами и принимают решения. «Обычно работает» недостаточно, когда у агента есть доступ к вашим ключам API, базе данных и клиентам.

Формальная верификация доказывает, что ни одно возможное исполнение не нарушает свойства безопасности. Не «мы проверили 10 000 случаев». Все. Доказательство того, что агент не может повысить привилегии, не вероятностное. Оно математическое.

Ссылки

• Доказательства: github.com/hanzoai/proofs
• Статьи: github.com/hanzoai/papers — 34 исследовательские работы с 2014 по 2026 год
• Сайт: proofs.hanzo.network

Формальная верификация охватывает всю экосистему Hanzo, от шлюза ИИ до инфраструктуры агентов. См. также hanzoai/proofs.