Özet: Yapay zeka çağında yazılımın güvenli olduğunu matematiksel olarak kanıtlamayı hedefleyen &Truth, 70 milyon dolarlık tohum yatırımla gizlilikten çıktı. Stanford ve Singapur Ulusal Üniversitesi kökenli şirket, her programlama dilindeki kodu doğrulayacak evrensel bir sistem geliştiriyor.
ABD ve Singapur merkezli &Truth, 29 Ekim 2026’da gizli çalışma döneminin (stealth) sona erdiğini duyurdu. 2026 başında kurulan şirket, 70 milyon dolar tohum yatırım aldı. Bu tutar, TCMB’nin 30 Ekim kuruyla yaklaşık 3,5 milyar TL ediyor.
Şirket, yatırımın “yapay zeka güvenliği ve girişim sermayesi alanındaki öncü isimlerden” geldiğini açıkladı. Ancak yatırımcıların adlarını paylaşmadı. Duyuru, şirketin resmi basın bülteninde yer alıyor.
&Truth tohum yatırımı neyi finanse ediyor?
&Truth, bir kamu yararı şirketi (public benefit corporation) olarak kuruldu. Şirketin hedefi, kodu okuyup güvenli, emniyetli ve doğru olduğunu matematiksel olarak kanıtlayan bir “evrensel doğrulama makinesi” yapmak. Kanıtların herkes tarafından bağımsız kontrol edilebilmesi amaçlanıyor.
Bu yaklaşımın adı biçimsel doğrulama (formal verification). Yöntem onlarca yıldır var, ancak pahalı olduğu için birkaç kritik sistemle sınırlı kaldı. Şirkete göre yapay zeka bu süreci 100 kat veya daha fazla hızlandırıyor. &Truth’un kanıt otomasyonu ise buna 100 kat daha ekliyor.
Şirket ayrıca “şartname fabrikası” adını verdiği bir teknoloji geliştiriyor. Bu araç, iş gereksinimlerini kesin biçimsel şartnamelere çeviriyor. Altyapı, açık kaynaklı kanıt sistemi Lean ve CSLib üzerine kuruluyor.
Kurucular ve ekip
Şirketin kurucu ortağı ve eş CEO’su Clark Barrett, Stanford Üniversitesi’nde bilgisayar bilimi profesörü. Barrett, açık kaynaklı cvc5 otomatik akıl yürütme motorunun proje lideri. Kurucu ortak ve bilim direktörü Ilya Sergey ise Singapur Ulusal Üniversitesi’nde VERSE Lab’in kurucusu.
Üçüncü kurucu Chris Hsu, eş CEO ve icra kurulu başkanı. Hsu daha önce Kilometre Capital’in CEO’su ve Citadel Investment Group’ta genel müdürdü. Ekipte Lean 4’ün ortak mimarlarından Sebastian Ullrich de bulunuyor.
Barrett, “Yapay zeka matematiği dönüştürdü, çünkü Lean ve Mathlib ona akıl yürütme için kesin bir dil verdi” dedi. Hsu ise “Yapay zeka çağında yüzde 99 güvenli bile kesinlikle bozuk demektir” dedi.
Sektör ve rakipler
&Truth’un çıkış noktası, yapay zekanın ürettiği kodun incelenebilenden hızlı yayılması. Bu sorun, yapay zeka kodlamasının güvenlik riskleri tartışmasında sık gündeme geliyor. Şirket, test ve kod incelemesinin gerekli olduğunu ama garanti vermediğini savunuyor.
Lean tabanlı yapay zeka alanında Harmonic ve Axiom Math gibi girişimler de var. Bu şirketler ağırlıkla matematiksel kanıta odaklanıyor. &Truth ise aynı yaklaşımı her dildeki yazılıma taşımayı hedefliyor.
Biçimsel doğrulamada daha dar alanlarda çalışan şirketler de bulunuyor. Certora, akıllı sözleşmeleri doğruluyor. Yapay zeka güvenliğinde ise yatırım iştahı yüksek; Cyera kısa süre önce 400 milyon dolarlık tur almıştı.
Türkiye’ye etkisi: Yazılım ihracatçıları için yeni güven ölçütü
Türk yazılım şirketleri bankacılık, savunma ve kamu gibi alanlarda kritik sistemler geliştiriyor. Bu sektörlerde yapay zekayla yazılan kodun kanıtlanabilir güvenliği, ihracatta yeni bir müşteri talebine dönüşebilir. Matematiksel kanıt, bağımsız denetimi kolaylaştırıyor.
Fırsat, Lean ve biçimsel yöntemlerde yetkin mühendislerde. Biçimsel yöntemler, uzmanlık isteyen dar bir alan. Türk üniversitelerinden çıkan araştırmacılar için uzaktan çalışma ve ortak araştırma kapısı açılabilir.
Geliştiriciler arasında yapay zeka kodlamasına güven de tartışılıyor. Bu konudaki bulguları Coddy geliştirici anketi haberimizde aktarmıştık.
Girişimci için çıkarımlar
Birinci çıkarım: Akademik derin teknoloji, doğru zamanlamayla büyük tohum turları çekebiliyor. &Truth, onlarca yıllık bir yöntemi yapay zekanın getirdiği hızla yeniden konumlandırdı.
İkinci çıkarım: Yapay zeka ajanlarıyla kod yazan her ürün, “kod doğru mu” sorusuyla karşılaşacak. Kurumsal otomasyonda büyüyen Serval’in 150 milyon dolarlık turu da bu talebin ölçeğini gösteriyor.