Anthropic, Claude'un 123 açık kaynak kitaplığının çökmediğini kanıtlayan biçimsel kanıtlar yazdığını söylüyor

Theorem ile iş birliği yapan Anthropic, Claude'u kullanarak 100'den fazla gerçek dünyadaki açık kaynak kitaplığında montaj dili düzeyinde (RISC-V) güvenlik özelliklerini kanıtladığını söylüyor. Şirkete göre bu, üretim yazılımlarını bu düzeyde biçimsel olarak doğrulamak için yapay zekânın büyük ölçekte ilk kullanımı.

Anthropic'e göre:

• Kanıtlananlar: 123 OSS-Fuzz kitaplığındaki 239 fuzz testi giriş noktası için programlar, 64 MB'ın altındaki her girdiyle normal biçimde sonlanıyor; bellek güvenliği hatası ya da başarısız iddia oluşmuyor. Bu sonuç, tek iş parçacıklı statik bir ikili dosya, sabit bellek bütçesi ve Linux çalıştıran bir RISC-V CPU varsayımları altında geçerli. Kanıtlar toplamda yaklaşık 180 milyon satır Rocq kodundan oluşuyor ve Rocq kanıt denetleyicisi tarafından doğrulandı.
• Yöntem: Her kitaplığın mevcut fuzz testi bir belirtime dönüştürüldü ("bu test asla çökmez") ve Claude, bulduğu hataları düzeltirken kanıtı yazdı. Anthropic, bunun bir fuzz testinin muhtemelen bulamayacağı, nadiren gereken 20 MB'lık bir girdiyle tetiklenen sınır dışı yazma hatası gibi yüzlerce hatayı ortaya çıkardığını ve libexpat'te CVE-2026-56132'yi yeniden bulduğunu söylüyor.
• Diğer deneyler: Claude, Linux çekirdeğinin zlib uygulamasının RFC 1950 belirtimiyle x86 ikili dosya düzeyinde eşleştiğini kanıtladı ve davranışı 1,7 milyon rastgele programın %99,95'inde CPython ile eşleşen bir Rust Python yorumlayıcısı oluşturdu. Anthropic ayrıca, yaygın kullanılan bir PDF okuyucuda yapılan biçimsel doğrulama girişimlerinin, bir haftada genellikle bir yılda bildirilen kadar güvenlik hatası ortaya çıkardığını söylüyor.
• Maliyet: Kanıtlar yüz milyonlarca token gerektirebilir. Anthropic, 36 küçük doğrulama görevinde Opus 5.5'in görevlerin yarısını Opus 5'e göre yaklaşık %40 daha az token kullanarak kanıtladığını; kanıtları paylaşan ajanların ise %17 daha az token kullandığını söylüyor.

Anthropic, kanıtların bir alt kümesini ve RISC-V ile Linux semantiklerini yayımlıyor. Theorem, aynı işlem hattını diğer açık kaynak projelerinde çalıştırmayı teklif ediyor ve kendi kodunuzu doğrulamak için bir Claude skill yayımlıyor. Anthropic, bunun kitaplıkların hatasız olduğunu göstermediğini belirtiyor: geriye kalan hatalar, güvenilen bileşenlerde ya da kanıtların kapsamı dışında olabilir.