&Truth привлекает $70 млн посевного финансирования для создания универсальной машины верификации кода

&Truth — общественно полезная корпорация, разрабатывающая технологии для математического доказательства безопасности программного обеспечения, — вышла из режима скрытой разработки 29 октября 2026 года, сообщив о привлечении $70 млн посевного финансирования и планах создать то, что компания называет универсальной машиной верификации кода.

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

Автоматизация доказательств на базе Lean

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

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

&Truth использует Lean — систему доказательств с открытым исходным кодом — и Mathlib, библиотеку, содержащую более двух миллионов строк математических определений и теорем, а также такие технологии с открытым исходным кодом, как CSLib. По словам компании, цель — создать универсальный формальный язык для программного обеспечения: математические модели языков программирования и систем, методы доказательства и точные спецификации, позволяющие автоматически выполнять верификацию на разных языках. &Truth сообщила, что сотрудничает с Lean Focused Research Organization и намерена открыть исходный код своих базовых библиотек.

Сооснователь и сопредседатель совета директоров Кларк Барретт заявил, что Lean и Mathlib дали ИИ точный язык для рассуждений в математике, тогда как в программной инженерии сопоставимой основы не было. Сооснователь и директор по науке Илья Сергей отметил, что доверие к программному обеспечению должно основываться на доказательствах, которые можно независимо проверить, а не на словах какой-либо компании.

Основатели и две штаб-квартиры

Барретт — профессор информатики имени Корбела в Стэнфордском университете, один из основателей и содиректор Stanford Center for AI Safety, директор Stanford Center for Automated Reasoning, один из создателей CSLib и руководитель проекта по разработке движка автоматизированных рассуждений cvc5. Сергей основал лабораторию VERSE Lab в Национальном университете Сингапура и стал одним из создателей верификаторов с открытым исходным кодом Veil и Velvet. Сооснователь, сопредседатель совета директоров и исполнительный председатель Крис Сю входит в стратегический консультативный совет Lean FRO и возглавляет Infinitude Foundation; ранее он был генеральным директором Kilometre Capital и управляющим директором Citadel Investment Group.

В объявлении также названы Грегори Малеча, ранее возглавлявший направление формальных методов в BlueRock Security и сыгравший ключевую роль в разработке архитектуры фреймворка верификации BRiCk; Себастьян Ульрих, один из создателей архитектуры Lean 4 и сооснователь Lean Focused Research Organization; Линус Ли, ранее управлявший партнёр Kilometre Capital; и Дрю Харман, бывший коммерческий директор Fastino Labs и операционный партнёр Insight Partners и Shasta Ventures. &Truth заявила, что опирается на десятилетия исследований в области формальной верификации и автоматизированных рассуждений, проводившихся в Стэнфордском университете и Национальном университете Сингапура.

Штаб-квартира &Truth в США находится в Пало-Альто, а международная штаб-квартира — в Сингапуре. По словам компании, сингапурский офис значительно расширит деятельность в области исследований, инженерной разработки, создания продуктов и выхода на рынок. В объявлении старший вице-президент и содиректор направления Digital Industry Singapore Лоу Джин Ён заявил, что открытие штаб-квартиры позволит укрепить возможности Сингапура в сфере доверия и безопасности и укрепит позиции страны как базы для компаний, разрабатывающих заслуживающий доверия ИИ.

На сайте компании также опубликована дискуссия за круглым столом с Леонардо де Моурой, создателем Lean, вице-президентом и заслуженным научным сотрудником AWS, и Симоне Северино, членом стратегического консультативного совета Lean FRO и заслуженным инженером Google.

В сопутствующих эссе изложены аргументы компании

В сопутствующем эссе от 29 октября 2026 года Сю подробно описал тенденции, которые, по мнению компании, делают верификацию неотложной задачей. Он привёл слова генерального директора Google Сундара Пичаи о том, что сейчас 75% нового кода в Google создаётся ИИ и утверждается инженерами, а также результаты тестирования Veracode за 2026 год: модели ИИ не справились почти с половиной задач по программированию, в которых имела значение безопасность. В эссе также упоминается кампания, проведённая в сентябре 2026 года: злоумышленник задействовал сотни ИИ-агентов, чтобы взломать 395 организаций в 48 странах, используя уязвимости в широко распространённом программном обеспечении для управления печатью. Кроме того, приводится рекордное число уязвимостей программного обеспечения — 14 959, опубликованных в сентябре 2026 года. По оценке автора эссе, это в 3,5 раза больше, чем годом ранее.

В эссе рассказывается о ранних этапах развития формальной верификации: первоначальное доказательство корректности микроядра seL4 потребовало примерно 20 человеко-лет работы экспертов над примерно 8 700 строками кода; в 2015 году в рамках программы DARPA HACMS seL4 встроили в вертолёт Boeing Unmanned Little Bird, систему управления полётом которого не смогла взломать профессиональная красная команда, получившая несколько недель доступа; а в сентябре 2026 года модель ИИ, разработанная Anthropic, за 11 дней формализовала в Lean полное доказательство последней теоремы Ферма. Также отмечается, что ранее в 2026 году Ким Моррисон, старший инженер по исследовательскому программному обеспечению в Lean FRO, с помощью Claude от Anthropic и при минимальном участии человека создал версию библиотеки сжатия zlib на Lean и доказал, что она всегда точно восстанавливает данные, которые сжала.

В эссе приводятся слова создателя Lean Леонардо де Муры: «Тестирование укрепляет уверенность. Доказательство даёт гарантию».

В своём втором эссе, опубликованном 29 октября 2026 года, Сергей объясняет, как устроена верификация программ, начиная с работы Алана Тьюринга «Проверка большой программы» (1949), в которой предлагалось, чтобы программисты сопровождали код точными утверждениями, каждое из которых мог бы проверить специальный инструмент. В эссе описываются спецификации, инварианты циклов и доказательства, проверяемые в Lean, а также говорится, что цель &Truth — дать разработчикам возможность получать независимо проверяемые подтверждения, например формальное доказательство в Lean, по такой цене, чтобы верификация стала обычной частью разработки.

&Truth описывает своё долгосрочное видение как переход от «вайб-кодинга» к «верифицированному кодингу»: код, созданный ИИ, математически проверяется до развёртывания, ИИ-агенты работают в средах с доказуемо заданными границами, устаревшее программное обеспечение безопасно модернизируется, а критически важная инфраструктура защищена независимо проверяемыми математическими гарантиями.