Формальная верификация пошла в масштаб: Claude доказал свойства кода 123 библиотек

Доказать математически, что код делает ровно то, что написано в спецификации, умеют давно, но делали это руками и годами. Anthropic 29.10.2026 отчиталась о другом масштабе: Claude провёл такую проверку по скомпилированному коду 123 открытых библиотек и нашёл в них баги, которые прятались годами.

Не хотите разбираться сами? Внедряем ИИ в ваш бизнес: задачи без лимита, одна цена в месяц, отмена в любой момент.

Проверяют не исходник. Свойства безопасности Claude доказывал для кода после компиляции, то есть для того, что реально выполняется. Apple сверяет свою криптобиблиотеку corecrypto со спецификацией инструментами Lean, Rocq и Isabelle, и её команда безопасности говорит прямо: часть найденных так проблем иначе обнаружить было нельзя.

Кто за это платит

Упирается всё не в инструменты, а в людей. Apple добавляет новый код осторожно, иначе на разбор доказательств не хватает сил. Открытые библиотеки сейчас проверяют на деньги ИИ-лабораторий: Beneficial AI Foundation разбирала код шифрования на гранте Anthropic.

Майкл Розенберг, мейнтейнер curve25519-dalek, оценивает такую схему коротко: «полагаться на добрую волю ИИ-компаний точно не стоит».

Деньги в тему пришли в тот же день. 29.10.2026 из стелса вышла &Truth с seed-раундом на $70 млн и целью построить «универсальную машину верификации», которая читает код на любом языке и выдаёт независимо проверяемое доказательство его корректности. Команду собрали из Clark Barrett (руководит проектом SMT-решателя cvc5 в Stanford), Ильи Сергея (VERSE Lab в NUS) и Sebastian Ullrich (со-архитектор Lean 4), ещё двое пришли из Citadel и BlueRock Security.

Компания обещает, что доказательства, на которые уходили годы и месяцы, будут занимать часы и минуты. Раскладка её заявки такая: 100x даёт применение ИИ и ещё 100x собственная технология, включая автогенерацию спецификаций. Продукта у &Truth сегодня нет, на andtruth.com висит только форма подписки на будущие демо, базовые библиотеки компания обещает открыть.

Что можно запустить сегодня

Velvet. Проверяет императивные программы с циклами, массивами и изменяемым состоянием, живёт в Lean 4, сделан в лаборатории Ильи Сергея. Сначала ставится Lean 4 через elan, дальше `git clone https://github.com/verse-lab/velvet.git`, `cd velvet` и `lake build`. В свой проект Velvet подключается блоком `[[require]] name = "velvet", git = "https://github.com/verse-lab/velvet.git", rev = "main"` в lakefile.toml, а документация советует начинать с Sqrt.lean, потом Loops.lean про инварианты и StateT.lean про контракты с состоянием.

Veil. Доказывает распределённые протоколы, и его дают попробовать прямо в браузере на try.veil.dev, без установки. Авторы из NUS представили Veil на CAV 2025.

CSLib. Библиотека для Lean, среди соавторов тот же Clark Barrett. Подключается блоком `[[require]] name = "cslib", scope = "leanprover", rev = "main"` в lakefile.toml и командой `lake update cslib`.

В гонке с 2026 года идут ещё Theorem, Pramaana Labs и VerifAIX, но, по счёту самой &Truth, её раунд больше их раундов вместе взятых.