💻 ИИ доказал корректность кода? Не совсем
Статья Sid Trehan (Keller AI, 10.11.2026): верификация ИИ-кода подтверждает лишь соответствие математической спецификации при заявленных допущениях, а не бизнес-требованиям и не тайминг-атакам.
🌍 Верификация выходит из ниши критических систем в рабочий процесс: Anthropic и Theorem Labs сгенерировали на Claude ~180 млн строк доказательств в Rocq — crash-freedom для 239 точек входа в 123 библиотеках OSS-Fuzz, попутно найдены сотни багов, включая логический, живший 10+ лет. GitHub Next и Microsoft Research выпустили PDD Kit: агент пишет код, Verus проверяет по спецификации.
👤 Доказано конкретное свойство при конкретных допущениях, а не «код без багов»: читайте спецификацию и trusted assumptions — в PDD Kit sign-off cards на SQLite, bcrypt, JWT.
Источник 1: https://kellerai.io/resources/ai-proved-your-code-correct Источник 2: https://www.anthropic.com/research/formal-verification