Формальная верификация может доказать свойство кода агента только в пределах заданной модели

«В коде нет ошибок» не годится как задание на проверку. Ошибка определяется требованием. Для расчёта можно задать правило округления и предел суммы, для оплаты: повтор одного события не создаёт второй доступ. Это разные проверяемые свойства.

Поэтому задачу для агента сначала переводят в точное условие. Указывают допустимые входы, ожидаемый результат, состояние до и после операции. Кто написал реализацию, человек или агент, не меняет смысл гарантии.

Тест показывает поведение на выбранном примере. Формальное доказательство устанавливает свойство в принятой математической модели. В неё входят и правила языка, и представление чисел, и ограничения входа. Модель бывает описанием алгоритма или семантикой самого проверяемого кода.

Вернёмся к функции, которая всегда возвращает ноль. В официальном учебнике Dafny функция модуля числа сначала обязана выдавать неотрицательный результат. Постоянный ноль этому условию удовлетворяет, хотя модуль положительного числа должен равняться самому числу.

Проверяющий инструмент выполнил свою работу. Недостаточно было требования. Для бизнеса это разница между «скидка не отрицательная» и «скидка рассчитана по утверждённому тарифу». Первое условие допускает и нулевую скидку для любого заказа.

Предусловия тоже нужно утверждать. Если доказательство действует только для неотрицательных сумм, вход с отрицательной суммой обязан отклоняться до расчёта. Предпосылку нельзя молча распространить на данные, которые ей не соответствуют.

Модель платёжного процесса может описывать события и смену состояний, не содержать код обработчика. В TLC выбирают конечную конфигурацию и свойства для перебора. Успешный полный прогон относится к ней; прерванный поиск такой гарантии не даёт.

Инженеры AWS в статье от 29 сентября 2014 года отдельно разбирают разрыв между проверенным дизайном и исполняемой реализацией. Они также описывают пропущенную ошибку живости в менеджере блокировок: это свойство не проверяли. Проверка дизайна полезна, но её предмет надо назвать.

Для оплаты «доступ не создаётся повторно» относится к безопасности: запрещённое событие не случится. «Оплативший в итоге получит ссылку» относится к живости: нужное событие случится. Последнее требует условий о повторах, очереди и восстановлении почтового сервиса.

В vibecoding.ru инженер ведёт машину нашего проекта. Мы удерживаем правила тестами, проверками типов и ревью. Формальной верификации нашего кода и клиентского кейса у нас нет. Зелёный набор проверок не называем доказательством корректности продукта.

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

Ответственность за ошибки требует и решения о выпуске, и правил реакции на сбой. Здесь полезен более узкий урок: из каждой поломки выделить свойство, которое потеряли. Потом выбрать проверку именно этого свойства, а не добавить ещё один общий статус «всё зелёное».

Для первой оценки выбирайте узел, у которого дорогое последствие и точное правило: расчёт суммы, ограничение риска, допустимый переход состояния. Такой предмет проще описать, чем обещание «проверить весь продукт». Это редакционный критерий выбора, не оценка срока или стоимости.

Узкая функция всё равно требует условий вокруг неё. Расчёт может быть верен для целых копеек, а вызывающий код передавать дробные числа с другим округлением. Модель переходов может быть верна, а реализация выполнять операции в ином порядке.

Глубина доказательства тоже различается. У seL4 есть доказательства до уровня кода и для отдельных конфигураций до бинарного представления, но опубликованы и предпосылки об аппаратуре и загрузке. Для вашего проекта решение о выпуске должно учитывать такую же явно названную границу.

Согласуйте правила для агентов и отдельное задание проверяющему. Агент может подготовить модель и доказательство. Его уверенное объяснение не заменяет принятого результата инструмента и ревью спецификации: слабое требование останется слабым независимо от автора.

Просите исходники спецификации и проверяемого объекта, версии инструментов и команду воспроизведения. В отчёте должны быть статус завершения, допущения и исключения. Если проверяли только абстрактный дизайн, отдельно назовите способ проверки соответствия реализации.

Тайм-аут не равен найденной ошибке, а сообщение «контрпримеров пока нет» не равно завершённой проверке. Уточняйте, закончился ли выбранный режим успешно, какая конфигурация была проверена и воспроизводится ли этот результат после агентной правки.

Сохраните проверку рядом с изменением. Следующая правка должна повторить её или явно пересмотреть свойство и предпосылки. Если случилась поломка вне модели, зафиксируйте исключённое условие и решите, надо ли расширить модель. Так результат кормит следующий цикл разработки.

Чтобы обсудить следующую задачу, переходите на страницу услуг. Начните с критичной функции и последствия её ошибки. Применимость формальной проверки, выполнение и способ проверки согласуются по этой задаче.

Подписка на агентную разработку «Один проект» стоит 250 000 ₽/мес по состоянию на 8 октября 2026. Это разработка одного продукта в одном потоке задач. Услугу математического доказательства мы не заявляем; применимость проверки критичной функции нужно оценить отдельно.

1. Выберите дорогое последствие и запишите точное свойство, которое его исключает.

2. Утвердите допустимые входы, среду и предпосылки до запуска проверки.

3. Назовите объект: модель, исходный код или бинарное представление. Обоснуйте связь с тем, что выпускаете.

4. Принимайте исходники и воспроизводимый завершённый результат для конкретной версии.

5. Сохраните проверки за границей доказательства и возвращайте новые поломки в требования.