Claude Artık Kod Yazmakla Kalmıyor, Doğruluğunu da İspatlıyor

Bir yazılımın "doğru çalıştığını" nasıl bilirsiniz? Normalde testler yaparsınız: programı farklı girdilerle çalıştırır, hata verip vermediğine bakarsınız. Ama bu, çorbanın tuzunu anlamak için birkaç kaşık tatmaya benzer — kazanın dibinde kalan kısmı hiç kontrol etmemiş olursunuz. Formal doğrulama (formal verification) dediğimiz yöntem ise tam tersini yapar: matematiksel bir ispatla, kodun her koşulda doğru çalıştığını kanıtlamaya çalışır. Sorun şu ki bu işlem inanılmaz derecede pahalıdır. Küçük bir işletim sistemi çekirdeği olan seL4'ü formal olarak doğrulamak için bir uzman ekip 20 kişi-yılı harcamıştı. Bu yüzden yöntem şimdiye kadar yalnızca Airbus'ın uçuş yazılımları gibi hayati önem taşıyan birkaç istisnai projede kullanılabildi.

Anthropic'in "Frontier Red Team"i, Theorem adlı ortağıyla birlikte bu işi yapay zeka modeli Claude'a devretti. Sonuç çarpıcı: Claude, Google'ın güvenlik açığı tarama projesi OSS-Fuzz kapsamındaki 123 açık kaynak kütüphane için sadece birkaç hafta içinde yaklaşık 180 milyon satır ispat kodu üretti. Claude burada yeni kod yazmadı; var olan yazılımı aldı, kütüphanelerin çökme (crash) testlerini matematiksel problemlere dönüştürdü, derlenmiş makine kodunu analiz etti ve kapsamlı ispatlar ortaya koydu. Bu ispatları da Rocq adlı bağımsız bir doğrulama programı otomatik olarak kontrol ediyor. Anthropic'e göre süreç neredeyse hiç insan denetimine ihtiyaç duymuyor — tabii altyapıyı ve matematiksel temelleri Theorem'deki insan mühendislerin kurduğunu unutmamak lazım.

İşin en ilginç tarafı şu: Claude ispat üretirken yolda rastladığı hataları kendi kendine düzeltebildi. Yaygın kullanılan bir PDF okuyucusunu doğrularken ekip, bir haftada o yazılım için normalde yılda bildirilen kadar güvenlik açığı buldu. Başka bir uygulamada ise Claude, on yıldan fazla süredir fark edilmemiş bir mantık hatasını yakaladı. Bunlar, standart testlerin genellikle kaçırdığı türden sorunlar — çok büyük bir dosya boyutu ya da çok özel bir erişim sırası gibi nadir koşullarda ortaya çıkıyorlar.

Bu Ne Anlama Geliyor?

Anthropic burada dürüst davranıyor: "formal olarak doğrulanmış" demek "hatasız" demek değil. İspatlar yalnızca belirli koşullar altında geçerli — tek bir işlemci mimarisi, tek iş parçacıklı (single-threaded) programlar ve 64 megabayttan küçük girdiler gibi sıkı sınırlar var. Gerçek dünyada bu kütüphaneler farklı donanımlarda, farklı yapılandırmalarda çalışıyor. Ayrıca maliyet hiç küçümsenecek gibi değil: tek bir ispat için yüzlerce milyon token harcanabiliyor, bu da işlemi şimdilik herkesin erişebileceği bir araç olmaktan uzaklaştırıyor.

Yine de trend yönü net. Daha önce yazdığımız gibi, Anthropic kodlama ve güvenlik konusunda agresif bir strateji izliyor ve bu proje o stratejinin bir parçası. Küçük bir test turunda, ispatların yeniden kullanılabilir olduğu ve yeni modellerin giderek daha verimli çalıştığı görüldü: Opus 5.5, Opus 5'e göre yüzde 40 daha az token harcayarak ispatların yarısını çözebiliyor. Bu, maliyetin zamanla düşeceğinin bir işareti. Eğer yapay zeka hem kod yazıp hem de bu kodun belirli koşullar altında güvenli olduğunu kanıtlayabilirse, soru artık "Yapay zeka programlayabilir mi?" değil, "Yazdığı kodun güvenli olduğunu kanıtlayabilir mi?" haline geliyor. Theorem'in yol haritası da şimdiden glibc, OpenSSL ve cURL gibi internetin temel taşlarını hedefliyor — bu üçü de dünya genelinde milyarlarca cihazda sessizce çalışan, kritik altyapı parçaları.

Bu arada konuyu güvenlik denetimiyle karıştırmayın: bu, kodlama ajanlarının kendi güvenlik gözetimini kapatması gibi riskli bir otomasyon değil, tam tersine insan denetimine ihtiyacı azaltırken güveni artırmayı hedefleyen bir yaklaşım.

Türkiye'ye Etkisi

Türk yazılım ekipleri de dahil dünyadaki neredeyse her geliştirici, günlük işinde glibc, OpenSSL veya cURL gibi kütüphanelere dolaylı olarak bağımlı. Bu altyapı bileşenleri formal olarak doğrulanırsa, bunun faydası tek bir ülkeyle sınırlı kalmaz; küresel ölçekte daha az sıfırıncı gün (zero-day) açığı, daha güvenilir sunucular ve bankacılık altyapısı anlamına gelir. Türkiye'de özellikle finans ve kamu sektöründe açık kaynak kütüphanelere duyulan güvenin artması, bu tür projelerin dolaylı ama somut bir kazanımı olabilir.