Rust и QUIC уже делают то, к чему ИИ только подбирается

Пока все спорят про агентов и автокодинг, в системной разработке quietly происходит очень важная вещь. Люди начинают нормально проверять сложные системы, а не надеяться на тесты.

Команда Адольфо Очагавии взяла QUIC-симулятор на базе quinn и попыталась убедиться, что он вообще работает корректно. Не на простых кейсах, а на произвольных сетях, включая сценарии уровня Земля–Марс.

Обычные тесты быстро закончились. Покрыть такие сценарии руками невозможно.

Они пошли другим путём. Сначала зафиксировали на бумаге, что считается корректным поведением. Затем встроили audit-лог прямо в симуляцию. После этого написали отдельный verifier, который прогоняет каждую симуляцию и проверяет её автоматически.

Ключевой момент в том, как это реализовано. Основную логику вообще не трогали. Проверка вынесена в отдельный слой. Сам verifier достаточно простой, его можно прочитать и понять без погружения в систему. Поверх этого появились golden-тесты, которые ловят регрессии.

Это выглядит как практическая версия того, о чём сейчас много говорят в контексте ИИ. Не просто генерировать код или тесты, а формализовать поведение системы и проверять его на уровне свойств.

Если переносить на AI-системы, то это ровно та же проблема. У нас есть агенты, пайплайны, куча состояний и внешних эффектов. И почти нет нормальной верификации. Всё держится на эвристиках и наблюдении.

Этот кейс хорошо показывает, куда двигаться дальше. Не усложнять архитектуру, а добавлять слой проверяемости поверх неё.

Разбор здесь
https://ochagavia.nl/blog/a-real-world-case-of-property-based-verification/