Summary
Anthropic and Theorem used Claude to generate ~180M lines of Rocq proofs for 123 OSS-Fuzz libraries at RISC-V binary level, finding long-hidden bugs and arguing LLM-scaled formal verification can approach fuzzing practicality.
PreScreening Notes
- Score: 8/10 (high)
- Recency: published 2026-10-22T22:54:43Z, ~7.2h old at screening — passes 48h gate
- Domain fit: ai, software — formal methods at scale
- Newsworthiness: ~180M lines Rocq proofs for OSS-Fuzz libs; Anthropic research on LLM-assisted verification
- Duplicates: none in active pipeline
Evaluation Report
News Value Assessment
| Dimension | Rating | Notes |
|---|---|---|
| Timeliness | ★★★★★ | Fresh Anthropic research post |
| Impact | ★★★★☆ | Shifts cost curve for security-critical OSS assurance |
| Prominence | ★★★★☆ | Anthropic + Theorem; OSS-Fuzz ecosystem |
| Proximity | ★★★★★ | High interest for Turkish backend/security engineers |
| Novelty | ★★★★★ | Scale (180M LOC proofs) is genuinely new benchmark |
Audience Fit
- Primary audience: Software developers, security researchers, formal-methods curious engineers.
- Actionability: Understand when LLM+proof assistants complement fuzzing; links to OSS supply chain.
- Topic connection: Bridges AI hype and rigorous engineering — signature NewsAgency software+AI crossover.
Risk & Ethics Assessment
- Verification: Primary on anthropic.com/research; reproducibility details in paper.
- Fact-checking: > [!warning] Clarify which bugs were net-new vs known classes; avoid overstating “solved verification.”
- Ethics: Credit Theorem/OSS-Fuzz contributors; not a product launch.
Publication Strategy
- Format:
deep-dive(1200+ words) — Rocq, RISC-V binary level, methodology, limits. - Related wiki: anthropic, claude, formal verification concept page (analysis).
Suggested Angle
“Fuzzing’e rakip mi?” değil: LLM’lerin Rocq kanıt üretimini ölçekleyerek OSS-Fuzz kütüphanelerinde gizli hataları nasıl surfaced ettiği; 180M satır kanıtın ne anlama geldiği ve Türk geliştirici için pratik çıkarım (supply chain, when to adopt formal methods).
Source Analysis
Corroborated with additional raw feeds listed in Research Notes.
Research Notes
Additional sources
- 2026-10-22-anthropic-llm-formal-verification (primary)
- 2026-10-22-anthropic-formal-verification-appendix (theorem statements, scope limits)
Verified / unverified
- Verified: 239 entry points / 123 libraries; ~180M lines checked Rocq; RISC-V ASan binaries ≤64 MiB inputs
- Verified: Claude found bugs despite massive prior fuzzing
-
Does not replace fuzzing on production arch/dynamic builds
Context
- Shifts cost curve for OSS assurance; complements supply-chain-security for C/C++ deps
Related wiki
Editorial Notes
- Onaylanan çerçeve:
deep-dive(1200+ kelime); teknik ama erişilebilir; «fuzzing’in yerini aldı» iddiasından kaçın. - Reporting talimatları: Rocq, RISC-V ASan binary, 123 kütüphane / ~180M satır kanıt; Theorem ortaklığı; üretim mimarisi/dinamik build sınırlarını !warning ile vurgula; OSS-Fuzz bağlamı.
- Başlık önerileri: «Anthropic: LLM’ler formal verification’ı OSS ölçeğine taşıyor»; «180 milyon satır Rocq kanıtı: OSS-Fuzz kütüphanelerinde gizli hatalar»
- Zorunlu noktalar: Metodoloji özeti; fuzzing ile tamamlayıcı ilişki; geliştirici için supply-chain çıkarımı; kaynak: anthropic.com/research.
Draft Article
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.