Спеки, правила и скиллы для AI-агентов: что агент должен знать о проекте, спеки по агрегатам и петля сверки.
Почему любой код агента нельзя проверить на любое правило, какие три способа делают проверку конечной, как граница агрегата из event storming становится постом проверки, как по проверяемости выбрать размер ограниченного контекста и почему первую рамку важно уметь дёшево сдвигать.
Что говорит теорема Райса и почему проверка поведения программы упирается в проблему остановки. Предикат о тексте и о поведении, доказательство на примере с оплатой, связь с парадоксом брадобрея и три рамки, которые делают проверку точной.
Vitest или Jest: настройка, место запуска, стиль проверок. Когда брать Vitest на Vite, оставить Jest или хватит QUnit в браузере. Таблица и вопросы.
Как найти состояние гонки в коде: модель на Quint перебирает порядки действий и показывает цепочку, где правило ломается. Примеры и пределы метода.
Тест проверяет придуманный сценарий, model checking перебирает все порядки действий. Что ловят QUnit, Jest, Vitest и что Quint, TLA+, Alloy. Как выбрать.
TLA+, Alloy или Quint: что описывает каждый, как записывается, чем проверяется и кому подходит. Парные сравнения, таблица и вопросы.