Kodun Doğruluğunu Matematikle Kanıtlayan &Truth, 70 Milyon Dolar Tohum Yatırımı Aldı

Palo Alto ve Singapur merkezli &Truth, 29 Ekim 2026'da gizlilik döneminden çıktığını ve 70 milyon dolar tohum yatırımı aldığını duyurdu. 2026 başında kurulan şirket, herhangi bir programlama dilinde yazılmış kodun güvenli, emniyetli ve doğru olduğunu matematiksel olarak kanıtlamayı hedefliyor. Yapay zekânın her gün milyonlarca satır kod ürettiği bir dönemde, "bu kod gerçekten doğru mu?" sorusuna kesin yanıt arıyor.

&Truth ne yapıyor?

Şirket, ürününü "evrensel doğrulama makinesi" olarak tanımlıyor. Bu sistem, kodu okuyup güvenli ve doğru çalıştığını kanıtlamayı ve bu kanıtların herkes tarafından bağımsız olarak kontrol edilebilmesini amaçlıyor. Yaklaşımın temelinde açık kaynaklı Lean kanıt sistemi ve CSLib gibi açık teknolojiler var.

Şirketin açıkladığı başlıca bileşenler şunlar:

• Kanıt otomasyonu: &Truth'a göre yapay zekânın kanıt üretimine sağladığı hızlanmanın üzerine 100 kat daha ekleyerek süreleri yıllar ve aylardan saatlere, dakikalara indiriyor.
• Şartname fabrikası: İnsanların niyetini ve iş gereksinimlerini ölçekli biçimde formal şartnamelere dönüştüren teknoloji.
• Evrensel formal sözlük: Programlama dilleri ve sistemlerin matematiksel modelleri, kanıt teknikleri ve şartnamelerden oluşan bir kütüphane.

Şirket, temel kütüphanelerini açık kaynak olarak yayımlamayı planladığını ve Lean Focused Research Organization ile birlikte çalıştığını da belirtiyor.

Kurucular kim?

&Truth'un kurucu ekibi akademi ve finans dünyasından isimlerden oluşuyor:

• Clark Barrett (kurucu ortak ve eş CEO): Stanford Üniversitesi bilgisayar bilimi profesörü, Stanford Yapay Zekâ Güvenliği Merkezi'nin kurucu eş direktörü ve cvc5 motorunun proje lideri.
• Ilya Sergey (kurucu ortak ve bilim direktörü): Singapur Ulusal Üniversitesi'ndeki VERSE Lab'in kurucusu.
• Chris Hsu (kurucu ortak, eş CEO ve yönetim kurulu başkanı): Kilometre Capital'in eski CEO'su ve Citadel Investment Group'un eski yöneticisi.

Ekipte Lean 4'ün mimarlarından Sebastian Ullrich de yer alıyor. Şirket, kâr amacının yanında kamu yararını da gözeten bir "public benefit corporation" olarak yapılandırıldı. Yatırımcıların isimleri açıklanmadı; şirket yalnızca yatırımın yapay zekâ güvenliği ve girişim sermayesi alanında öncü isimlerden geldiğini söylüyor.

Rakipler ve benzer girişimler

&Truth, yapay zekâ ile formal doğrulamayı birleştiren tek girişim değil. TechInside'ın derlemesine göre Harmonic ve Axiom Math, Lean üzerinde matematiksel kanıtlara odaklanıyor; Certora ise akıllı sözleşmelerin doğrulanması üzerine çalışıyor. &Truth'u ayıran nokta, herhangi bir programlama dilindeki genel yazılımı hedeflemesi. Digital Industry Singapore'un eş başkanlarından Low Jin Yong da yapay zekâ kullanımı yaygınlaştıkça güven ve güvenliğin daha önemli hale geleceğini, &Truth'un Singapur merkezinin ülkeyi güvenilir yapay zekâ çözümleri için bir üs haline getirmeye katkı sağlayacağını söyledi.

Kurucular ne diyor?

Clark Barrett, yapay zekânın matematiği dönüştürebilmesinin nedeninin Lean ve Mathlib'in ona akıl yürütme için kesin bir dil sağlaması olduğunu, yazılımın ise bugüne kadar böyle bir temelden yoksun kaldığını söylüyor. Ilya Sergey, yazılıma duyulan güvenin "herhangi bir şirketin sözüne, bizimki de dahil, değil; bağımsız olarak kontrol edilebilen kanıta" dayanması gerektiğini vurguluyor. Chris Hsu ise "Yapay zekâ çağında yüzde 99 güvenli olmak, kesinlikle bozuk olmak demektir" diyor.

Türkiye için anlamı

Formal doğrulama uzun süre havacılık ve çip tasarımı gibi niş alanlara sıkışmış, pahalı bir uzmanlık olarak görülüyordu. Yapay zekâ destekli kanıt üretimi bu maliyeti düşürürse, bankacılık, savunma ve kamu için yazılım geliştiren Türk şirketleri "kanıtlanabilir güvenlik" talebiyle daha sık karşılaşabilir. Lean ve formal yöntemler alanında çalışan Türk araştırmacılar ve mühendisler için de bu alan yeni iş ve iş birliği fırsatları anlamına gelebilir.