./новости · 29 июля 2026 г.
новость
Массовой формальной верификации не будет даже при ИИ-коде: спека нужна ради 1% случаев
источник: @gergelyorosz · X·
машинная выжимка · сверена с источником
Gergely Orosz
@gergelyorosz
Есть популярная теория: ИИ наконец сделает формальную верификацию массовой, потому что, когда код пишут машины, понадобится математическое доказательство корректности. Но случится ли это? Хиллел Уэйн - один из лучших, кто может ответить. Тайм-коды: 00:00 Вступление 04:32 The Crossover Project 11:37 В чём software engineering лучше 15:30 В чём традиционная инженерия лучше 18:17 Формальные методы 29:32 Что такое TLA+ и демо 36:58 TLA+ в Amazon 38:10 Как ломаются распределённые системы 41:03 Формальные методы и системное мышление 46:20 Зачем учить математику 50:23 Для чего TLA+ хорош, а для чего нет 52:50 Alloy: декларативный язык для моделирования софта 58:53 Другие инструменты формальных методов 1:01:24 Property-based тестирование 1:05:31 ИИ и потребность в формальной верификации 1:12:29 Logic for Programmers 1:14:35 Прогноз Хиллела 2025 года о влиянии ИИ 1:21:30 Книжная рекомендация Выпуск поддержали: • @AntithesisHQ - проверяйте корректность своей системы без ручного ревью и обычных интеграционных тестов, чтобы не ловить баги и падения. https://antithesis.com/pragmatic • @turbopuffer - векторный и полнотекстовый поисковый движок на объектном хранилище. Быстрый, дешёвый и отлично масштабируется. https://turbopuffer.com/pragmatic • @WorkOS - всё, что нужно, чтобы довести приложение до корпоративного уровня. https://workos.com/ Две вещи, которые в разговоре с Хиллелем показались мне особенно интересными: 1. Amazon нашла с помощью TLA+ баг, который почти невозможно найти без формальных методов. В статье How AWS uses formal methods команда AWS рассказала, что нашла сложный баг: кратчайший сценарий, который его воспроизводит, состоит из 35 шагов (!!). Баг незамеченным прошёл через подробное ревью дизайна, ревью кода и тесты. В AWS сделали вывод: если бы держались обычных подходов к тестированию, они бы его не нашли. 2. Почему тогда не верифицировать формально всё подряд? Потому что писать спеки в реальном мире - это кошмар. Даже простая задача «найти в папке файл с наибольшим числом строк» усложняется, когда моделируешь её формальными методами. Придётся отвечать на вопросы: смотрим на ASCII или UTF-8 переводы строк, что делать с нечитаемыми файлами, а что с симлинками? Без формальных методов можно написать простую проверку, которая права в 99%+ случаев. А формальные методы требуют кучи лишних усилий ради меньше чем 1% экзотических случаев!
· 5,4 тыс. просмотров
Кратчайший сценарий, который воспроизводит найденный в AWS баг, занимает 35 шагов. Гергей Орош выложил 29 июля разговор с Хиллелем Уэйном про формальные методы, 85 минут. Баг прошёл мимо подробного ревью дизайна, ревью кода и тестов: в AWS сделали вывод, что обычным тестированием его бы не выловили.
Почему это важно: Теорию про массовую верификацию повторяют с тех пор, как код начали писать агенты: машины пишут - значит, нужна математика корректности. Уэйн переносит вопрос в другое место: узкое горло не в проверке, а в спеке. Он берёт задачу «найти в папке файл с наибольшим числом строк» и показывает, во что она превращается в формальной модели: ASCII или UTF-8 переводы строк, нечитаемые файлы, симлинки. Обычная проверка на этой же задаче права в 99%+ случаев. Формальная забирает остаток меньше 1% и требует кучи лишних усилий. Ниша, где счёт сходится, при этом никуда не делась: 35-шаговый баг AWS - ровно она.
Что дальше: Блок про ИИ и потребность в верификации начинается на 1:05:31, прогноз Уэйна о влиянии ИИ - на 1:14:35. Проверить тезис на себе можно так: взять один инвариант своей распределённой части, описать его в TLA+ по демо с 29:32 и засечь, сколько времени ушло на спеку.
первоисточник