Anthropic, Claude’un 123 açık kaynak kütüphanede 239 giriş noktasının çökmediğini biçimsel olarak kanıtladığını açıkladı

Anthropic’in Frontier Red Team ekibi 22 Ekim’de, Claude ile büyük ölçekte biçimsel doğrulama yaptığı bir çalışmayı yayımladı. Theorem ile birlikte yürütülen çalışmada OSS-Fuzz projesindeki mevcut fuzz testleri, testin hiç çökmediğini söyleyen biçimsel şartnamelere çevrildi. Claude, 123 kütüphanedeki 239 giriş noktası için bu şartnameleri kanıtladı. Kanıtlara göre programlar 64 MB’tan küçük hiçbir girdide bellek güvenliği hatası vermiyor ve assertion denetimlerine takılmıyor. Kanıtlar derlenmiş RISC-V makine kodu üzerinde yazıldı ve Rocq kanıt denetleyicisiyle kontrol edildi. Anthropic bunu, yapay zekayla üretimdeki yazılıma biçimsel doğrulama uygulayan ilk büyük ölçekli çalışma olarak tanımlıyor.

Anthropic’e göre çalışma birkaç hafta sürdü ve toplam yaklaşık 180 milyon satır Rocq kanıtı üretildi. Tipik bir kanıt yaklaşık 600.000 satır tutuyor. Kanıt denemeleri sırasında yüzlerce hata ortaya çıktı ve Claude bunları yamaladı. Örnekler arasında yalnızca 20 MB civarındaki nadir girdilerde tetiklenen bir sınır dışı yazma hatası ve libexpat’teki CVE-2026-56132 açığının yeniden bulunması var. 36 küçük doğrulama görevinde Opus 5.5, görevlerin yarısını Opus 5’ten yaklaşık yüzde 40 daha az token harcayarak kanıtladı.

Anthropic, “biçimsel olarak doğrulanmış” ifadesinin “hatasız” anlamına gelmediğini vurguluyor. Kanıtlar tek iş parçacıklı, musl libc ile statik bağlanmış RISC-V programlarını varsayıyor. Kullanıcıların çoğu ise x86 ya da ARM üzerinde dinamik bağlanmış glibc kullanıyor. Her kütüphanenin tüm giriş noktaları doğrulanmadı ve bir kanıt yüz milyonlarca token gerektirebiliyor. Şirket, yamalanmamış hataları açığa çıkarabilecek kanıtları yayımlamıyor.