Anthropic'in Claude’u artık kod yazıyor ve otomatik olarak güvenliğini kanıtlıyor

Anthropic'in Claude modeli, Theorem iş birliğiyle mevcut açık kaynak kodlarını matematiksel olarak kanıtlayarak doğrulama sürecini otomatikleştirdi. Model, Google'ın OSS‑Fuzz projesindeki 123 kütüphane için çökme testlerini matematiksel problemlere dönüştürdü, derlenmiş makine kodunu analiz etti ve yaklaşık 180 milyon satır kanıt kodu üretti. Bu kanıtlar, bağımsız bir doğrulama aracı olan Rocq tarafından otomatik olarak kontrol edildi ve insan denetimine neredeyse ihtiyaç duyulmadı.

Claude, kanıt üretimi sırasında yüzlerce hatayı tespit etti ve kendisi düzeltti. Özellikle bir PDF okuyucusunun güvenlik açıkları bir haftada bir yıl içinde raporlanan hatalar kadar bulundu; başka bir kütüphanede ise on yıldan uzun süredir fark edilmemiş mantıksal bir hata ortaya çıkarıldı. Bu bulgular, geleneksel testlerin yalnızca belirli koşullarda ortaya çıkan hataları yakalayabildiğini, Claude'un ise çok daha nadir ve karmaşık senaryolarda da sorunları ortaya çıkarabildiğini gösteriyor.

Ancak Anthropic, bu tür "formel doğrulanmış" kodların hâlâ sınırlı koşullar altında geçerli olduğunu vurguluyor. Kanıtlar yalnızca belirli bir işlemci mimarisi, tek iş parçacıklı çalışma ve 64 MB altında giriş verileri için geçerli. Ayrıca bir kanıtın üretilmesi yüz milyonlarca token harcaması anlamına geliyor; toplam proje maliyeti açıklanmadı. Bununla birlikte, yeni nesil Claude Opus 5.5 modeli, önceki Opus 5 sürümüne göre kanıtların %40 daha az token harcayarak yarısını çözebildi.

Anthropic, bu teknolojinin gelecekte standart test süreçlerinin yerini alabileceğini ve kritik altyapı bileşenleri (glibc, OpenSSL, cURL gibi) için de uygulanabileceğini öngörüyor. AI tarafından üretilen kodun kendi güvenliğini kanıtlayabilmesi, geliştiricilerin inceleme süresini kısaltıp maliyetleri düşürürken, yazılım güvenliğine dair güveni de artırabilir.