&Truth získává v seed kole 70 milionů dolarů na vybudování univerzálního ověřovacího stroje pro kód

Společnost &Truth, veřejně prospěšná korporace vyvíjející technologie, které matematicky dokazují bezpečnost softwaru, vystoupila z utajení 29. října 2026. Oznámila, že získala 70 milionů dolarů v seedovém financování a plánuje vybudovat to, čemu říká univerzální ověřovací stroj pro kód.

V oznámení o svém uvedení na trh společnost uvedla, že vznikla na začátku roku 2026 a získala 70 milionů dolarů v seedovém kapitálu od skupiny osobností, které označila za průkopníky v oblasti bezpečnosti umělé inteligence a rizikového kapitálu. Dodala, že její ověřovací stroj vyvíjí tak, aby dokázal číst kód v libovolném programovacím jazyce a matematicky prokázat, že je bezpečný, zabezpečený a správný, přičemž předložené důkazy může kdokoli nezávisle ověřit.

Automatizace dokazování postavená na systému Lean

Formální verifikace existuje už desítky let, ale dosud byla nedostupná a nákladná, uvádí se v oznámení, protože odborníci museli důkazy vytvářet ručně, a tento postup se proto omezoval na několik kriticky důležitých systémů. Společnost uvedla, že umělá inteligence nyní urychluje práci na formálních důkazech nejméně 100krát a že její technologie pro automatizaci dokazování tento proces zrychluje ještě o dalších 100krát. Tvorba důkazů se tak zkracuje z let či měsíců na hodiny či minuty.

Společnost popsala také technologii, kterou nazývá „továrna na specifikace“. Ta podle ní umožňuje podnikům a vývojářům převádět lidské záměry a obchodní požadavky ve velkém měřítku na přesné formální specifikace a poskytovat záruky, které lze nezávisle ověřit a které se neopírají pouze o testování nebo tvrzení dodavatelů.

&Truth staví na systému Lean, otevřeném systému pro dokazování, a na knihovně Mathlib, která obsahuje více než dva miliony řádků matematických definic a vět, a také na technologiích s otevřeným zdrojovým kódem včetně CSLib. Cílem je podle společnosti vytvořit univerzální formální slovník pro software: matematické modely programovacích jazyků a systémů, techniky dokazování a přesné specifikace, které umožní automatizované ověřování napříč jazyky. &Truth uvedla, že spolupracuje s organizací Lean Focused Research Organization a zamýšlí zveřejnit své základní knihovny jako open source.

Spoluzakladatel a spoluředitel Clark Barrett uvedl, že Lean a Mathlib poskytly umělé inteligenci přesný jazyk pro matematické uvažování, zatímco softwaru dosud chyběl odpovídající základ. Spoluzakladatel a hlavní vědecký ředitel Ilya Sergey řekl, že důvěra v software by se měla opírat o nezávisle ověřitelné důkazy, nikoli o slovo kterékoli společnosti.

Zakladatelé a dvě hlavní sídla

Barrett je profesorem informatiky s titulem Corbel Professor na Stanford University, zakládajícím spolud ředitelem Stanford Center for AI Safety, ředitelem Stanford Center for Automated Reasoning, spolutvůrcem CSLib a vedoucím projektu automatizovaného systému pro uvažování cvc5. Sergey založil laboratoř VERSE Lab na National University of Singapore a podílel se na vytvoření open-source verifikátorů Veil a Velvet. Spoluzakladatel, spoluředitel a výkonný předseda představenstva Chris Hsu je členem poradního výboru Lean FRO Strategic Advisory Board a prezidentem Infinitude Foundation. Dříve působil jako generální ředitel Kilometre Capital a výkonný ředitel Citadel Investment Group.

V oznámení byli zmíněni také Gregory Malecha, který dříve vedl oblast formálních metod ve společnosti BlueRock Security a byl klíčovým architektem verifikačního rámce BRiCk; Sebastian Ullrich, spoluarchitekt systému Lean 4 a spoluzakladatel organizace Lean Focused Research Organization; Linus Lee, bývalý řídící partner Kilometre Capital; a Drew Harman, bývalý obchodní ředitel Fastino Labs a provozní partner ve společnostech Insight Partners a Shasta Ventures. &Truth uvedla, že navazuje na desítky let výzkumu formální verifikace a automatizovaného uvažování na Stanford University a National University of Singapore.

Sídlo společnosti &Truth v USA se nachází v Palo Altu a její mezinárodní centrála v Singapuru. Společnost uvedla, že tamní kancelář výrazně rozšíří v oblastech výzkumu, vývoje, produktů a obchodního rozvoje. Low Jin Yong, senior viceprezident a spoluvedoucí oddělení Digital Industry Singapore, v oznámení uvedl, že centrála prohloubí kapacity Singapuru v oblasti důvěry a bezpečnosti a posílí jeho postavení jako základny pro společnosti vyvíjející důvěryhodnou umělou inteligenci.

Na webových stránkách společnosti je také diskuse u kulatého stolu s Leonardem de Mourou, tvůrcem systému Lean, viceprezidentem a významným vědcem v AWS, a Simonem Severinim, členem poradního výboru Lean FRO Strategic Advisory Board a významným inženýrem ve společnosti Google.

Doprovodné eseje vysvětlují důvody, které společnost k projektu vedly

V doprovodné eseji z 29. října 2026 Hsu popsal trendy, kvůli nimž je podle společnosti ověřování naléhavé. Citoval vyjádření generálního ředitele Google Sundara Pichaie, podle něhož je nyní 75 % nového kódu v Google vytvořeno umělou inteligencí a schváleno inženýry, a testování společnosti Veracode z roku 2026, které zjistilo, že modely umělé inteligence selhaly téměř u poloviny programovacích úloh, v nichž byla důležitá bezpečnost. Esej dále zmiňuje kampaň ze září 2026, při níž útočník nasadil stovky agentů umělé inteligence a prostřednictvím zranitelností v široce používaném softwaru pro správu tisku pronikl do 395 organizací ve 48 zemích, a také rekordních 14 959 softwarových zranitelností zveřejněných v září 2026, což je podle eseje 3,5násobek počtu zveřejněného o rok dříve.

Esej připomíná dřívější milníky formální verifikace: původní důkaz mikrojádra seL4 si vyžádal zhruba 20 člověkoroků práce odborníků na přibližně 8 700 řádcích kódu; v roce 2015 bylo v rámci programu HACMS agentury DARPA začleněno seL4 do vrtulníku Boeing Unmanned Little Bird, jehož letové řízení nedokázal prolomit profesionální tým simulující útočníky, přestože měl několik týdnů přístup; a v září 2026 model umělé inteligence vyvinutý společností Anthropic za 11 dní v jazyce Lean formalizoval úplný důkaz Fermatovy poslední věty. Esej také uvádí, že začátkem roku 2026 Kim Morrison, vedoucí výzkumný softwarový inženýr v Lean FRO, s minimálním lidským vedením využil Claude od společnosti Anthropic k vytvoření verze kompresní knihovny zlib v jazyce Lean a dokázal, že vždy přesně obnoví data, která zkomprimovala.

Esej cituje tvůrce jazyka Lean Leonarda de Mouru: „Testování vzbuzuje důvěru. Důkaz poskytuje záruku.“

V druhé eseji zveřejněné 29. října 2026 Sergey vysvětluje, jak funguje verifikace programů, a začíná článkem Alana Turinga z roku 1949 „Checking a Large Routine“, v němž Turing navrhl, aby programátoři ke svému kódu připojovali přesná tvrzení, která by kontrolní nástroj mohl ověřovat jednotlivě. Esej popisuje specifikace, invarianty cyklů a důkazy kontrolované v jazyce Lean a uvádí, že cílem společnosti &Truth je umožnit vývojářům získat nezávisle ověřitelné důkazy, například formální důkaz v jazyce Lean, za cenu, díky níž se verifikace stane běžnou součástí vývoje.

&Truth popisuje svou dlouhodobou vizi jako přechod od „programování podle pocitu“ k „programování s ověřením“, při němž se kód generovaný umělou inteligencí před nasazením matematicky ověřuje, agenti umělé inteligence pracují v prostředích, u nichž lze prokázat, že jsou jejich možnosti omezené, zastaralý software se bezpečně modernizuje a kritická infrastruktura je chráněna nezávisle ověřitelnými matematickými zárukami.