70 milyon dolarlık bir tohum turu her yıl dikkat çekicidir. &Truth için bu aynı zamanda bir sav: biçimsel doğrulama — yazılımı test etmek yerine matematiksel olarak kanıtlamak — teoriden değil maliyetten tıkandı ve üretken yapay zekâ doğrudan bu maliyete saldırabilir.
Şirket 29 Ekim'de, Palo Alto ve Singapur merkezli bir kamu yararına şirket (PBC) olarak görünürlükten çıktı; 2026 başında kurulmuş. Kurucu ortaklar: Stanford profesörü ve Stanford Yapay Zekâ Güvenliği Merkezi eş direktörü Clark Barrett (eş-CEO), Singapur Ulusal Üniversitesi VERSE Laboratuvarı'nın kurucusu Ilya Sergey (baş bilim insanı) ve Chris Hsu (eş-CEO ve yönetim kurulu başkanı). &Truth yatırımcılarını açıklamadı, turun koşullarını da paylaşmadı.
Teknoloji, Lean kanıt sisteminin ve CSLib gibi açık kaynak projelerin üzerine kurulu. &Truth kendi modelini kanıt otomasyonuyla birleştirerek herhangi bir programlama dilindeki kodu okuyor ve güvenlik, emniyet ve doğruluk üzerine herkesin bağımsız olarak kontrol edebileceği iddialar üretiyor. Yanında bir 'şartname fabrikası' var: iş gereksinimlerini kesin biçimsel şartnamelere çeviren teknoloji. Pratikte işin zor yarısı bu, çünkü çoğu kod tabanı kodu getirir ama kullanılabilir bir şartname getirmez.
Turu taşıyan gösterim, ağustosta &Truth'a katılan Stanford araştırmacısı Chuyue Sun'dan geldi. Ekibi, Signal mesajlaşma uygulamasının şifreleme kodunun bir bölümünü yapay zekâyla biçimsel olarak doğruladı: yarım günden az çalışma, 500 dolardan az maliyet. Şirkete göre aynı iş, elle, üç deneyimli mühendise yaklaşık beş ay sürerdi.
'Köprüler, binalar çökmez, çünkü insanlar inşa etmeden önce matematik yaptı' dedi Sergey. 'Neden aynısını kod için yapmıyoruz? Matematiksel akıl yürütme teknolojisi zaten vardı, yalnızca ölçeklenmesi zordu.' Barrett ise yapay zekânın son dönemde açık matematik sanıtlarını kanıtlamasına paralellik kurdu: aynı biçimsel yöntemler yazılıma da uygulanabilir.
&Truth bir dalganın parçası. Nvidia'nın girişim kolunun da aralarında bulunduğu yatırımcılardan 295 milyon dolar toplayan rakip Harmonic, bu hafta C kodu ve Verilog donanım tasarımlarını doğrulayan Aristotle adlı ajanını tanıttı; Tensordyne ve Nvidia'nın onu değerlendirdiği aktarılıyor. Anthropic ile doğrulama girişimi Theorem, açık kaynak yazılımlarda yapay zekâ destekli hata avı ve Claude için bir doğrulama eklentisini birlikte duyurdu. Microsoft Research'ten ayrılan Madan Musuvathi, yapay zekâ sektöründeki güvenlik olaylarının ardından otomatik doğrulamayı ticarileştirmek için Truidic'i kurdu.
Kuşku bol ve hak edilmiş. Hata avı girişimi Antithesis'in CEO'su Will Wilson, biçimsel doğrulamayı tek başına 'bir tuzak' olarak niteledi: şirketi savunma sistemlerini doğrulamak için milyonlar harcadı ve test araçlarıyla yine de başka hatalar buldu. Ethereum'un yaratıcısı Vitalik Buterin, doğrulamanın güvenlik açıklarına panzehir olmadığı uyarısını yaptı. AWS'de seçkin bilim insanı Byron Cook, otomatik akıl yürütmenin müşterilerin bulut güvenliği kaygılarını hafiflettiğini söylüyor; ancak orta ölçekli şirketler Wired'a, doğrulama için haftalarca beklemenin geliştirmeyi yavaşlattığını ve doğrulama mühendisi bulmanın zor olduğunu söyledi.
Asıl iddia şu: kanıtların kusursuz olduğu değil, normal bir geliştirme döngüsünün içine girecek kadar ucuzladığı. Signal şifrelemesinin bir dilimi için yarım günün altında ve 500 doların altında bir maliyet, en azından aritmetiği ilginç kılıyor.
