Anthropic: LLM’ler formal verification’ı OSS ölçeğine taşıyor — 180 milyon satır Rocq kanıtı
anthropic, theorem ile yürüttüğü yeni araştırmada claude modellerinin formal-verification için kanıt üretimini ölçeklendirebildiğini gösteriyor: oss-fuzz kapsamındaki 123 açık kaynak kütüphanede 239 giriş noktası için RISC-V assembly seviyesinde güvenlik özellikleri kanıtlandı; toplamda yaklaşık 180 milyon satır Rocq kanıtı üretildi. Ekip, trilyonlarca fuzz çalışmasına rağmen yıllardır görülmeyen hataların da surfaced edildiğini yazıyor. Bu, «fuzzing bitti» anlamına gelmiyor; üretim mimarileri ve dinamik build’ler için sınırlar açıkça belirtiliyor.
Ana Gelişme
Araştırma yazısı 22 Ekim’de anthropic.com/research üzerinde yayımlandı. Motivasyon net: AI saldırganlar kod hatalarını daha kolay bulup exploit edebiliyor; klasik test ve fuzzing tek başına «hatasız» garanti vermiyor. Formal verification teoride bu garantiyi sunar, ancak uzman yılları gerektirdiği için çoğu projede pratik değildi.
İşbirliğinde Claude, derlenmiş RISC-V instruction’ları üzerinde «crash olmaz» ve ilgili güvenlik özelliklerini ispatladı. Tipik bir kanıt paketi yaklaşık 600.000 satır Rocq; median 18.000 RISC-V instruction’lı binary’ler için. Varsayımlar: tek thread, statik binary, Linux üzerinde RISC-V, 64 MB altı girdi, sabit bellek bütçesi — AddressSanitizer (ASan) ile derlenmiş binary’ler.
Bulunan hata sınıfları fuzzer’ların nadiren tetiklediği köşeler: ~20 MB girdilerle counter underflow, 64 MB girdi ve multi-GB bellek gerektiren OOB okumalar, çoklu handle çağrı dizileri. Ekip ayrıca libexpat’te CVE-2026-56132’nin yeniden keşfini sayıyor. zlib için RFC uyumluluğu x86 binary seviyesinde kanıtlandı; Rust’ta Verus ile doğrulanmış Python alt kümesi yorumlayıcısı (CPython ile 1,7M rastgele programda %99,95 davranış eşleşmesi) ve yaygın bir PDF okuyucuda latent mantık hataları da raporlanıyor.
Neden Önemli?
Açık kaynak supply-chain-security özellikle C/C++ bağımlılıklarında kritik. Türk backend ve güvenlik mühendisleri için mesaj: LLM + proof assistant hattı, formal methods’u yalnızca akademik örneklerden çıkarıp OSS-Fuzz ekosistemine taşıyor — maliyet eğrisini değiştiriyor. Bu hâlâ araştırma aşaması; ürün SLA’sı değil.
ai-cybersecurity tartışması genelde saldırı tarafını vurguluyor; bu çalışma savunma tarafında kanıt üretimini otomatikleştirmeyi öne çıkarıyor. Theorem, aynı pipeline’ı diğer OSS projeleri için çalıştırmayı ve Claude skill yayınlamayı duyurdu; Anthropic güvenilir bileşenler ve tamamlanmış Rocq kanıtlarının bir kısmını paylaşmayı planlıyor (yamalanmamış hata sızdırmayan kısımlar).
Teknik Detaylar
Rocq (eski adıyla Coq), etkileşimli theorem prover; kanıtlar makine tarafından kontrol edilir. Assembly seviyesi seçimi, kaynak kodu ile dağıtılan binary arasındaki derleyici/optimizasyon boşluğunu kapatmayı hedefler — ancak spesifikasyon hâlâ «bu binary bu özelliği sağlar» iddiasıdır.
OSS-Fuzz, Google destekli sürekli fuzzing altyapısı; trilyonlarca execution bu kütüphanelerde önceden koştu. Yeni bulgular, fuzzing’in gücünü küçümsemek için değil; formal ve fuzzing’in tamamlayıcı olduğunu göstermek için sunuluyor.
Kanıtlar RISC-V ASan statik binary ve belirtilen girdi sınırları için geçerli. Dağıtımdaki x86/ARM, glibc sürümü, dinamik linking veya multi-thread davranışı kapsam dışı olabilir. ASan tüm bellek hatalarını yakalamaz. Tüm library entry point’leri verify edilmedi.
Verimlilik notları: daha yeni Opus modelleri benchmark verification görevlerinde ~%40 daha az token kullandı; paylaşılan proof workspace’leri solo ajanlara göre %17 token tasarrufu sağladı.
Metodoloji özet akışı:
flowchart LR A[OSS-Fuzz library] --> B[RISC-V ASan binary] B --> C[Claude proof generation] C --> D[Rocq checker] D --> E[Property proved or bug found]
Bağlam
fuzzing on yıllardır endüstri standardı; formal-verification ise havacılık ve kritik embedded’da sınırlı çekirdekte kaldı. LLM’lerin kanıt iskeleti ve lemma üretiminde yardımcı olması, 2024–2026 araştırma literatüründe artan bir tema; Anthropic-Theorem çalışması bugüne kadar raporlanan en büyük üretim OSS kanıt hacmi olarak konumlanıyor.
anthropic Frontier Red Team imzalı yazı, ürün lansmanı değil; yine de claude’un enterprise güvenlik anlatımına teknik derinlik ekliyor. Kernel LKML sızıntısı ve Tor exit haberleriyle aynı haftada, «güvenlik kanıtı» ile «güvenlik süreci hatası» yan yana okunabilir.
Geliştirici çıkarımı: bağımlılık seçiminde SBOM, patch latency ve fuzz coverage yeterli; yüksek riskli native kütüphanelerde formal spec + proof assistant pilotu artık tamamen hayal değil — ama ekip Rocq/Verus uzmanlığı ve spec yazımı maliyetini hesaba katmalı.
Sonraki Adımlar
Topluluk, paylaşılan kanıt artefaktlarının tekrarlanabilirliğini ve mainline patch’lerle binary yeniden derleme döngüsünü izleyecek. Regülatörler ve büyük tech firmalar OSS güvence için AI+formal hibrit programları değerlendirebilir.
Fuzzing’i durdurmayın; formal layer’ı CI’da «yüksek riskli değişiklik» kapısına koymayı düşünün. Bu çalışma fuzzing’in yerini aldı iddiasını desteklemiyor — tam tersine, uzun süredir fuzz’lanmış kodda bile formal yaklaşımın fark yaratabildiğini gösteriyor.