&Truth, Kod İçin Evrensel Doğrulama Makinesi Geliştirmek Üzere 70 Milyon Dolarlık Tohum Yatırımı Aldı

Yazılımın güvenli olduğunu matematiksel olarak kanıtlayan teknolojiler geliştiren kamu yararına çalışan şirket &Truth, 29 Ekim 2026’da faaliyetlerini kamuoyuna duyurarak 70 milyon dolarlık tohum yatırımını ve kendi deyimiyle kod için evrensel bir doğrulama makinesi geliştirme planını açıkladı.

Kuruluş duyurusunda şirket, 2026’nın başlarında kurulduğunu ve öncü yapay zekâ güvenliği ve risk sermayesi liderleri olarak tanımladığı bir gruptan 70 milyon dolar tohum sermayesi aldığını söyledi. Şirket, doğrulama makinesinin her programlama dilindeki kodu okuyacak ve kodun güvenli, emniyetli ve doğru olduğunu matematiksel olarak kanıtlayacak şekilde geliştirildiğini; bu kanıtların herkes tarafından bağımsız olarak denetlenebileceğini belirtti.

Lean Üzerine Kurulu İspat Otomasyonu

Duyuruda, biçimsel doğrulamanın onlarca yıldır var olduğu, ancak uzmanların ispatları elle oluşturması gerektiğinden bugüne kadar erişilmesi güç ve pahalı olduğu, bu nedenle uygulamanın yalnızca az sayıda kritik sistemle sınırlı kaldığı belirtildi. Şirket, yapay zekânın biçimsel ispat çalışmalarını artık 100 kat veya daha fazla hızlandırdığını ve ispat otomasyonu teknolojisinin süreci buna ek olarak 100 kat hızlandırarak ispat üretimini yıllar ya da aylar süren bir iş olmaktan çıkarıp saatlere veya dakikalara indirdiğini söyledi.

Şirket, ayrıca “belirtim fabrikası” adını verdiği teknolojiyi tanıttı. Şirketin açıklamasına göre bu teknoloji, işletmelerin ve geliştiricilerin insan niyetini ve iş gereksinimlerini geniş ölçekte kesin biçimsel belirtimlere dönüştürmesini sağlıyor; böylece testlere veya satıcıların iddialarına dayanmak yerine bağımsız olarak denetlenebilen güvenceler sunuyor.

&Truth, açık kaynaklı bir ispat sistemi olan Lean ve iki milyondan fazla satır matematiksel tanım ve teorem içeren bir kütüphane olan Mathlib’in yanı sıra CSLib gibi açık kaynaklı teknolojiler üzerine çalışıyor. Şirkete göre amaç, yazılım için evrensel bir biçimsel dil oluşturmak: programlama dillerinin ve sistemlerin matematiksel modelleri, ispat teknikleri ve diller arası otomatik doğrulamayı mümkün kılan kesin belirtimler. &Truth, Lean Focused Research Organization ile birlikte çalıştığını ve temel kütüphanelerini açık kaynak olarak yayımlamayı planladığını belirtti.

Kurucu ortak ve eş CEO Clark Barrett, Lean ile Mathlib’in yapay zekâya matematiksel akıl yürütme için kesin bir dil kazandırdığını, yazılım alanında ise buna eşdeğer bir temelin bulunmadığını söyledi. Kurucu ortak ve Baş Bilim Sorumlusu Ilya Sergey, yazılıma duyulan güvenin herhangi bir şirketin sözüne değil, bağımsız olarak denetlenebilir kanıtlara dayanması gerektiğini belirtti.

Kurucular ve İki Merkez

Barrett, Stanford University’de Corbel Bilgisayar Bilimleri Profesörü, Stanford Center for AI Safety’nin kurucu eş direktörü, Stanford Center for Automated Reasoning’in direktörü, CSLib’in ortak geliştiricisi ve cvc5 otomatik akıl yürütme motorunun proje lideridir. Sergey, National University of Singapore’da VERSE Lab’ı kurdu ve açık kaynaklı doğrulama araçları Veil ile Velvet’in ortak geliştiricisi oldu. Kurucu ortak, eş CEO ve Yönetim Kurulu İcra Başkanı Chris Hsu, Lean FRO Stratejik Danışma Kurulu üyesi ve Infinitude Foundation başkanıdır; daha önce Kilometre Capital’in CEO’su ve Citadel Investment Group’da yönetici direktör olarak görev yaptı.

Duyuruda ayrıca, daha önce BlueRock Security’de biçimsel yöntemler ekibine liderlik etmiş ve BRiCk doğrulama çerçevesinin temel mimarlarından biri olan Gregory Malecha; Lean 4’ün ortak mimarı ve Lean Focused Research Organization’ın kurucu ortaklarından Sebastian Ullrich; daha önce Kilometre Capital’de yönetici ortaklık yapmış Linus Lee ve Fastino Labs’ın eski baş ticari sorumlusu, ayrıca Insight Partners ve Shasta Ventures’da faaliyet ortağı olarak çalışmış Drew Harman’ın da adı geçti. &Truth, Stanford University ve National University of Singapore’da biçimsel doğrulama ve otomatik akıl yürütme alanlarında onlarca yıldır sürdürülen araştırmalar üzerine çalıştığını belirtti.

&Truth’un ABD’deki merkezi Palo Alto’da, uluslararası merkezi ise Singapur’dadır. Şirket, Singapur ofisinin araştırma, mühendislik, ürün ve pazara açılma çalışmaları genelinde önemli ölçüde büyütüleceğini belirtti. Digital Industry Singapore Eş Başkanı ve Kıdemli Başkan Yardımcısı Low Jin Yong, duyuruda merkezin Singapur’daki güven ve emniyet yetkinliklerini derinleştireceğini ve ülkeyi güvenilir yapay zekâ geliştiren şirketler için bir üs olarak güçlendireceğini söyledi.

Şirketin internet sitesinde ayrıca Lean’in mucidi, AWS’de başkan yardımcısı ve Seçkin Bilim İnsanı olan Leonardo de Moura ile Lean FRO Stratejik Danışma Kurulu üyesi ve Google’da Seçkin Mühendis olan Simone Severini’nin katıldığı bir yuvarlak masa söyleşisi yer alıyor.

Ek Yazılar Şirketin Gerekçelerini Ayrıntılandırıyor

Hsu, 29 Ekim 2026 tarihli eşlik eden bir yazıda, şirketin doğrulamayı acil hâle getirdiğini söylediği eğilimleri ayrıntılandırdı. Google CEO’su Sundar Pichai’nin, Google’daki yeni kodların %75’inin artık yapay zekâ tarafından üretildiği ve mühendislerce onaylandığı yönündeki sözlerine; ayrıca Veracode’un 2026’da yaptığı ve yapay zekâ modellerinin güvenliğin önemli olduğu kodlama görevlerinin neredeyse yarısında başarısız olduğunu ortaya koyan testlere atıfta bulundu. Yazıda ayrıca, Eylül 2026’da bir saldırganın yaygın olarak kullanılan yazdırma yönetimi yazılımlarındaki açıkları kullanarak 48 ülkede 395 kuruluşun sistemlerine sızmak için yüzlerce yapay zekâ aracısı konuşlandırdığı bir kampanyadan ve Eylül 2026’da yayımlanan rekor sayıdaki 14.959 yazılım güvenlik açığından söz ediliyor. Yazıya göre bu sayı, bir yıl önce yayımlananların 3,5 katı.

Makale, biçimsel doğrulama alanındaki önceki dönüm noktalarını anlatıyor: seL4 mikro çekirdeğinin ilk kanıtı, yaklaşık 8.700 satır kod için uzmanların toplamda yaklaşık 20 kişi-yılı süren çalışmasını gerektirdi; 2015’te DARPA’nın HACMS programı kapsamında seL4, Boeing’in Unmanned Little Bird helikopterine entegre edildi ve helikopterin uçuş kontrollerine haftalarca erişim olanağı tanınan profesyonel bir kırmızı takım bu kontrolleri aşamadı; Eylül 2026’da ise Anthropic tarafından geliştirilen bir yapay zekâ modeli, Fermat’nın Son Teoremi’nin eksiksiz kanıtını Lean’de 11 günde biçimselleştirdi. Makale ayrıca, 2026’nın başlarında Lean FRO’da kıdemli araştırma yazılım mühendisi olan Kim Morrison’ın, Anthropic’in Claude’unu asgari insan yönlendirmesiyle kullanarak Lean’de zlib sıkıştırma kütüphanesinin bir sürümünü geliştirdiğini ve bu sürümün sıkıştırdığı verileri her zaman eksiksiz olarak geri yüklediğini kanıtladığını belirtiyor.

Makale, Lean’in yaratıcısı Leonardo de Moura’nın şu sözlerine yer veriyor: “Test etmek güven verir. Kanıtlamak ise garanti sağlar.”

29 Ekim 2026’da yayımlanan ikinci bir makalede Sergey, program doğrulamanın işleyişini açıklarken Alan Turing’in 1949 tarihli “Checking a Large Routine” başlıklı makalesinden yola çıkıyor. Turing bu makalede, programcıların kodlarına, bir denetleyicinin ayrı ayrı doğrulayabileceği kesin iddialar eşlik ettirmesini önermişti. Makale; özellikleri, döngü değişmezlerini ve Lean’de denetlenen kanıtları ele alıyor ve &Truth’un amacının, geliştiricilerin Lean’de biçimsel bir kanıt gibi bağımsız olarak denetlenebilir kanıtları, doğrulamayı geliştirmenin olağan bir parçası hâline getirecek bir maliyetle elde etmesini sağlamak olduğunu belirtiyor.

&Truth, uzun vadeli vizyonunu “sezgisel kodlama”dan “kanıtlamalı kodlama”ya geçiş olarak tanımlıyor. Bu yaklaşımda yapay zekâ tarafından üretilen kod, devreye alınmadan önce matematiksel olarak doğrulanıyor; yapay zekâ ajanları sınırları biçimsel olarak kanıtlanabilir ortamlarda çalışıyor; eski yazılımlar güvenli biçimde modernize ediliyor ve kritik altyapı bağımsız olarak denetlenebilir matematiksel garantilerle korunuyor.