Kanıtlar, RISC-V işlemcileri için, yani bir çipin fiilen çalıştırdığı derlenmiş komutlar olan assembly kodu düzeyinde yazıldı.
Anthropic'e göre Claude, kütüphanelerdeki 239 giriş noktasının 64 MB'ın altındaki hiçbir girdide çökmeyeceğini gösterdi ve süreç boyunca bulduğu hataları düzeltti.
Şirket, bunu bildiği kadarıyla üretim aşamasındaki yazılımı bu düzeyde biçimsel olarak doğrulamak için yapay zekânın kullanıldığı ilk büyük ölçekli çalışma olarak tanımlıyor.
Kodun tanımlı kurallara uyduğunu matematiksel olarak kanıtlayan biçimsel doğrulama (formal verification), gerektirdiği çaba nedeniyle şimdiye kadar yalnızca kritik görev sistemlerinde pratik olabildi.
Anthropic, geliştirilmesi iki kişi-yıl, doğrulanması 20 kişi-yıl süren seL4 çekirdeğini örnek gösteriyor.
Bu çalışmada Claude, koda üretilmiş girdilerle yüklenen mevcut fuzz testlerini belirtimlere dönüştürdü; dolayısıyla tamamlanmış bir kanıt, o giriş noktasına yönelik fuzzing ile artık yeni çökme bulunamayacağı anlamına geliyor.
Şirket, süreçte yüzlerce hata ortaya çıktığını söylüyor.
Bunların arasında fuzzer'ların yakalaması olası olmayanlar da var: yalnızca yaklaşık 20 MB'lık ve nadir bir düzene sahip girdilerle tetiklenen bir bellek yazma hatası ile libexpat'taki CVE-2026-56132'nin yeniden keşfi bunlara örnek.
Anthropic, "biçimsel olarak doğrulanmış" ifadesinin hatasız anlamına gelmediğini vurguluyor. Kanıtlar, Linux üzerinde çalışan bir RISC-V işlemcide, sabit bellek bütçeli, tek iş parçacıklı statik bir ikili dosyayı varsayıyor; oysa kullanıcıların çoğu bu kütüphaneleri x86 veya ARM üzerinde çalıştırıyor. Kanıtlar ayrıca kütüphanelerin tamamını değil, yalnızca test edilen giriş noktalarını kapsıyor. Kalan risk, güvenilen bileşenlerde bulunuyor: RISC-V ve Linux modelleri, teorem ifadeleri ve Rocq kanıt denetleyicisi. Kanıtlar toplamda yaklaşık 180 milyon satır Rocq kodundan oluşuyor ve bunları üretmek yüz milyonlarca token gerektirebiliyor; ancak Anthropic, yeni modellerin daha azına ihtiyaç duyduğunu ve ajanların birbirinin kanıtlarını yeniden kullanmasına izin vermenin bir testte token kullanımını %17 azalttığını belirtiyor. Şirket, kanıtların bir alt kümesini ve güvenilen bileşenleri yayımlıyor; Theorem ise bu süreci diğer açık kaynak projeler için çalıştırmayı öneriyor ve geliştiriciler için bir Claude skill'i yayımladı.