30 сентября 2026 г.
Проверка кода агентами догоняет сборку: Depot нашёл race condition за 21 минуту
В кейсе Depot от 20 июля model checker за примерно 21 минуту перебрал 14 290 224 состояния и нашёл race condition, которую пропустили тесты и review. Агент перевёл перестройку garbage collector в TLA+, а проверка доказала 10 safety-инвариантов и 2 liveness-свойства.
Gergely Orosz
@gergelyorosz
В прошлый раз, когда создание софта ускорилось примерно в 10 раз, в начале 2000-х вместе с agile-движением, почти сразу резко вырос интерес к автоматическому тестированию: unit-тестам, TDD, XP и остальному. Сейчас разработка софта тоже легко ускорилась в 10 раз, и следом растёт такой же огромный интерес к автоматическому тестированию и верификации...
· 7,1 тыс. просмотров
Раньше ускорение разработки в начале 2000-х почти сразу подстегнуло интерес к unit-тестам, TDD и XP. Теперь ИИ-агенты ускорили сборку софта примерно в 10 раз, и следом растёт интерес к автоматической проверке и верификации.
Уже есть инструменты. Antithesis предлагает skills для ИИ-агентов через `npx skills add antithesishq/antithesis-skills`. Для запуска нужны Snouty CLI, Docker или Podman и npm. После `snouty login` Docker Compose или Kubernetes-конфигурацию можно проверить командой `snouty validate <./path/to/config>` до запуска теста. Приложение придётся собрать под x86-64, а зависимости, которым нужен интернет при старте, добавить в image ещё при сборке.
Проверяют модель. Плагин Z Spec для Claude Code от Punt Labs извлекает спецификации из кода, генерирует код из спецификаций, проверяет типы, запускает fuzzing и model checking через ProB. TLA+ имеет смысл для конкурирующих процессов, сложных транзакций, автономных workers и операций между системами без общей транзакции. Для обычного CRUD endpoint model checker не нужен. AWS применяет формальные спецификации и model checking для критичных систем с 2011 года: один баг с trace в 35 высокоуровневых шагов прошёл design review, code review и тестирование.
Чем быстрее ИИ-агенты пишут код, тем чаще проверка будет начинаться не после бага, а до запуска системы.
Первоисточник