&Truth залучає $70 млн на посівному раунді для створення універсальної машини верифікації коду

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

У повідомленні про запуск компанія заявила, що заснована на початку 2026 року й отримала $70 млн посівного капіталу від групи осіб, яких вона назвала ключовими діячами у сферах безпеки ШІ та венчурного капіталу. За словами компанії, її машину верифікації створюють для читання коду будь-якою мовою програмування та математичного доведення його безпечності, захищеності й коректності; ці докази кожен зможе перевірити самостійно.

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

Як зазначено в повідомленні, формальна верифікація існує вже десятиліттями, але раніше була недоступною та дорогою, оскільки фахівці мусили формулювати доведення вручну, тож її застосовували лише до кількох критично важливих систем. Компанія заявила, що ШІ тепер пришвидшує роботу над формальними доведеннями у 100 разів або більше, а її технологія автоматизації доведень — ще у 100 разів, скорочуючи їх створення з років або місяців до годин або хвилин.

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

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

Співзасновник і співгенеральний директор Кларк Барретт заявив, що Lean і Mathlib дали ШІ точну мову для математичних міркувань, тоді як у програмному забезпеченні бракувало подібного фундаменту. Співзасновник і директор із наукової роботи Ілля Сергій сказав, що довіра до програмного забезпечення має ґрунтуватися на доказах, які можна перевірити незалежно, а не на словах будь-якої компанії.

Засновники та два головні офіси

Барретт — професор комп’ютерних наук Corbel у Stanford University, співдиректор-засновник Stanford Center for AI Safety, директор Stanford Center for Automated Reasoning, співтворець CSLib і керівник проєкту автоматизованого механізму міркувань cvc5. Сергій заснував VERSE Lab у National University of Singapore та став співтворцем інструментів верифікації з відкритим вихідним кодом 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 заявила, що спирається на десятиліття досліджень у сфері формальної верифікації та автоматизованих міркувань, проведених у Stanford University та National University of Singapore.

Головний офіс &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 році в межах програми HACMS агентства DARPA систему seL4 інтегрували у вертоліт Boeing Unmanned Little Bird, систему керування польотом якого професійна команда з тестування на проникнення, маючи кілька тижнів доступу, не змогла зламати; а у вересні 2026 року модель ШІ, розроблена Anthropic, за 11 днів формалізувала в Lean повний доказ Великої теореми Ферма. Також зазначено, що раніше у 2026 році Кім Моррісон, старший інженер-дослідник програмного забезпечення в Lean FRO, за мінімального втручання людини скористався Claude від Anthropic, щоб створити версію бібліотеки стиснення даних zlib для Lean і довести, що вона завжди точно відновлює дані, які стиснула.

У статті наведено слова творця Lean Леонардо де Мури: «Тестування додає впевненості. Доказ гарантує результат».

У другій статті, опублікованій 29 жовтня 2026 року, Сергій пояснює механізми верифікації програм і починає з праці Алана Тюрінга «Перевірка великої програми» 1949 року, у якій пропонувалося, щоб програмісти супроводжували код точними твердженнями, кожне з яких міг би перевірити засіб перевірки. У статті йдеться про специфікації, інваріанти циклів і докази, перевірені в Lean, а також зазначено, що мета &Truth — дати розробникам змогу отримувати докази, які можна перевірити незалежно, наприклад формальний доказ у Lean, за такої вартості, щоб верифікація стала звичайною частиною розробки.

&Truth описує своє довгострокове бачення як перехід від «вайб-кодування» до «верифікаційного кодування», за якого код, створений ШІ, математично перевіряють перед розгортанням, агенти ШІ працюють у середовищах із доведеними межами ізоляції, застаріле програмне забезпечення безпечно модернізують, а критично важливу інфраструктуру захищають математичні гарантії, які можна перевірити незалежно.