Компания &Truth вышла из тени 29 октября 2026 года и раскрыла seed-раунд на $70 млн для создания машины универсальной проверки кода. Компания, основанная в начале 2026 года как public benefit corporation, обещает читать код на любом языке программирования и математически доказывать его безопасность и корректность. Инвесторов она описывает как лидеров в области безопасности ИИ и венчурного капитала. Для бизнеса заявление важно потому, что ИИ уже пишет большую часть нового кода, а тестирование закрывает лишь часть дефектов.
Seed-раунд и машина проверяемых доказательств
Компания противопоставляет формальную верификацию тестированию и заверениям поставщиков. Вместо отчетов о покрытии тестами клиент получает доказательства, которые может независимо проверить любая сторона. По заявлению &Truth, ИИ уже ускорил работу над формальными доказательствами в 100 раз и более, а ее технология автоматизации дает еще стократное ускорение, сокращая работу с лет и месяцев до часов и минут. Второй элемент — технология specification factory, переводящая намерения людей и бизнес-требования в точные формальные спецификации в промышленных масштабах. Штаб-квартиры находятся в Пало-Альто и Сингапуре, причем офис в Сингапуре будет расширен по направлениям исследований, разработки, продукта и продаж.
Техническая основа — открытая система доказательств Lean и библиотека Mathlib из более чем двух миллионов строк математических определений и теорем, а также открытые технологии, включая CSLib. Цель &Truth — единый формальный словарь для софта: математические модели языков и систем, методы доказательств и точные спецификации, позволяющие автоматизировать проверку между языками. Компания сотрудничает с Lean Focused Research Organization и намерена выпустить базовые библиотеки в open source. Долгосрочная концепция описана как переход от vibe-coding к veri-coding, когда созданный ИИ код проверяют до запуска, а агенты работают в доказуемо изолированных средах.
Формальная верификация существует десятилетиями, но применялась лишь в нескольких критических системах, поскольку доказательства вручную строили эксперты и это стоило дорого. Классический пример — микроядро seL4: исходное доказательство для около 8 700 строк кода потребовало около 20 человеко-лет, позже систему использовали в вертолете Boeing Unmanned Little Bird по программе DARPA HACMS, защиту которого не смогла взломать профессиональная red team. Аргумент срочности строится на новом масштабе: по словам Сундара Пичаи, 75% нового кода в Google теперь создает ИИ, а тесты Veracode 2026 года показали провалы моделей почти в половине задач, связанных с безопасностью. В сентябре 2026 года опубликовали 14 959 уязвимостей, в 3,5 раза больше, чем годом ранее, а злоумышленник с помощью сотен ИИ-агентов атаковал 395 организаций в 48 странах через софт для управления печатью.
Что проверяемый код дает компаниям
Для компаний, внедряющих код, созданный ИИ, практический эффект — другая форма приемки: проверяемая гарантия вместо отчета о тестах. Крупные предприятия с регулируемыми системами, встроенным софтом и критической инфраструктурой смогут добавить верификацию в контроль выпуска новых сервисов, действий агентов и модернизации старых систем. Небольшие компании без специалистов по формальным методам получат доступ к такому контролю, если он придет как автоматизированный сервис на общих библиотеках. Ценность проявляется в закупках и аудите, где доказательство в Lean дает артефакт, который внутренняя безопасность и внешние проверяющие могут подтвердить без повторения всей работы.
Ограничения остаются существенными, и поставщику следует задать прямые вопросы. Неясно, какие языки, фреймворки и свойства систем машина покрывает в первую очередь, насколько полными должны быть спецификации и что происходит при неполных или меняющихся бизнес-требованиях. Приведенные примеры, включая формализацию доказательства Великой теоремы Ферма в Lean за 11 дней моделью Anthropic и версию библиотеки сжатия zlib в Lean, собранную с помощью Claude, показывают возможности, но сами по себе не доказывают стабильную промышленную производительность. Покупателям следует спросить о порядке проверки доказательств, интеграции в конвейер разработки, учете сторонних зависимостей и правах на спецификации. Сама новость еще не означает, что проверенный код уже доступен как продукт.
Маркером станет публикация базовых библиотек в open source и первые пилотные проверки с измеримыми сроками и масштабом. У команды серьезный вес: профессор Stanford Кларк Барретт, основатель VERSE Lab Илья Сергей, соавтор Lean 4 Себастьян Ульрих и создатель Lean Леонардо де Моура в круглом столе, а также поддержка Сингапура через Лоу Джин Йонга. Если независимые инженеры воспроизведут доказательства в Lean за часы, верификация станет требованием закупок. Если выпуск задержится, она останется исследовательским обещанием.
