Anthropic: Claude, 123 Kütüphanede Güvenlik Özelliklerini Kanıtladı

Anthropic, 22 Ekim 2026’da Theorem ile iş birliği içinde Claude’un 123 açık kaynaklı kütüphanedeki 239 fuzz testi giriş noktası için RISC-V assembly kodu düzeyinde güvenlik özelliklerine ilişkin makine tarafından denetlenmiş biçimsel kanıtlar ürettiğini bildiren bir araştırma yayımladı.

Anthropic’e göre Claude, bulduğu hataları giderdi ve ardından programların 64 MB’ın altındaki her girdi ile modellenen her Linux işletim sistemi yanıtı ve bellek düzeni için, bellek güvenliği hatalarına yol açmadan veya iddiaları ihlal etmeden normal şekilde sonlanacağını kanıtladı. Kanıtlar, programın Linux kullanan bir RISC-V CPU’da, sabit bellek bütçesiyle tek iş parçacıklı statik ikili dosya olarak çalıştığını varsayıyor. Anthropic, kanıtların yaklaşık 180 milyon satır Rocq kodundan oluştuğunu; ortanca uzunluğu 18.000 RISC-V komutu olan ikili dosyaları kapsayan tipik bir kanıtın yaklaşık 600.000 satır tuttuğunu söyledi. Şirket, kendi bilgisi dahilinde bunun, yapay zekâyı üretim yazılımlarına assembly kodu düzeyinde biçimsel doğrulama uygulamak için kullanan ilk büyük ölçekli çalışma olduğunu belirtti.

Kanıtların bir bölümü ile bunların dayandığı RISC-V ve işletim sistemi semantikleri GitHub’da yayımlanıyor. Anthropic, proje için oluşturulan ve henüz kamuya açık olmayan güvenilir bileşenleri, yama gerektirmeyen fuzz testlerine ilişkin eksiksiz kanıtları ve kanıtlayamadığı fuzz testlerinin belirtimlerini de yayımladığını; yamalanmamış bir hatayı açığa çıkarabilecek kanıtları ise yayımlamadığını söyledi.

Fuzz Testlerini Biçimsel Kanıtlara Dönüştürmek

Bu yaklaşım, her kütüphanenin mevcut derlenebilir fuzz testini tek bir kuralı kodlayan biçimsel bir belirtime dönüştürüyor: Test, 64 MB’ın altındaki hiçbir girdide çökmüyor. Belirtim, Theorem’in RISC-V komut kümesi ve Linux süreçlerine ilişkin biçimsel semantikleri kullanılarak derlenmiş RISC-V komutları üzerinden tanımlanıyor; Rocq kanıt denetleyicisi de tamamlanan her kanıtı belirtime göre doğruluyor. Anthropic’e göre bu yaklaşım, geliştiricilerin güvenmesi gereken bileşenleri yalnızca üç öğeyle sınırlıyor: RISC-V ve Linux süreçlerinin biçimsel modelleri, teoremlerin tam ifadeleri ve Rocq denetleyicisinin kendisi.

Anthropic, bu süreci Google’ın uygun açık kaynak projelerine sürekli fuzz testi sağlayan ve C ile C++ programlarını, belleğe hatalı erişildiğinde programı çökerten bir araç olan AddressSanitizer ile otomatik olarak enstrümante eden OSS-Fuzz girişimindeki yüzlerce projeye uyguladığını söyledi. 22 Ekim 2026 tarihli bir ekte kanıtlanan teoremin tamamı açıklanıyor: 64 MiB’ın altındaki tüm girdiler ve tüm bellek düzenleri için, ne ASan ile enstrümante edilmiş ikili dosya ne de sade ikili dosya hata verir, çalışmayı durdurur veya modellenmemiş davranış sergiler; ayrıca ikisi de aynı okuma ve yazma izlerini, çıkış davranışını ve son dosya sistemi durumunu üretir.

Ek bölümde, Claude’un çalışma sırasında yaklaşık bir milyar satır Rocq kodu yazdığı ve bunların yaklaşık 180 milyon satırının kanıt denetleyicisinden geçtiği belirtiliyor. cJSON’un 391 satırlık ayrıştırıcı giriş noktası için 630.000 satırlık bir kanıt oluşturulurken, bağlantılı kodu 51.000 satır olan fftw3 için 480.000 satırlık bir kanıt oluşturuldu. Claude’un kanıtı tamamlamadan önce kodda yama yapmasına izin verildiğinden Anthropic, yamaları puanlamada dezavantajlı kıldığını, yamaların hangi girdileri değiştirdiğini kanıtlamaya ek puan verdiğini ve ödül sisteminin istismar edilmesini önlemek için yamaları kayda geçirip denetlediğini söyledi.

Kanıtlama Girişimleri Sırasında Bulunan Hatalar

Anthropic, kanıtlama girişimlerinin yüzlerce hatayı ortaya çıkardığını ve bunların çoğunun bir fuzz testinin bulmasının pek olası olmadığı hatalar olduğunu bildirdi. Claude, bir kütüphanenin giriş noktasını kanıtlarken, bir sıkıştırma açıcıda sınır dışı yazmaya yol açan bir sayaç taşması buldu; ancak bu hata yalnızca yaklaşık 20 MB büyüklüğündeki girdilerde ve nadir, belirli bir bellek düzeninde ortaya çıkıyordu. Diğer bulgular arasında 64 MB’lık girdi ve 2 GB’tan fazla bellek gerektiren bir görüntü çözücüde sınır dışı okuma, aynı dosyaya ait iki tanıtıcı üzerinden belirli bir çağrı dizisi gerektiren sınır dışı okuma ve derin biçimde iç içe geçmiş girdi gerektiren libexpat’teki CVE-2026-56132’nin yeniden keşfi yer aldı.

Claude ayrıca, bir uygulamanın hangi dosyaları yükleyebileceğine ilişkin her zaman uygulanmayan bir kısıtlama da dahil olmak üzere, çökmeye yol açmayan mantık hataları buldu. Anthropic, yaygın olarak kullanılan ve kritik öneme sahip çeşitli uygulamalardaki doğrulama girişimlerinin, on yılı aşkın süredir gizli kalmış, daha önce bilinmeyen bir mantık hatasını ortaya çıkardığını söyledi. Şirket ayrıca, yaygın olarak kullanılan bir PDF okuyucuyu doğrulama çalışması sırasında, genellikle bir yılda bildirilen sayıda güvenlik hatasını tek bir haftada bulduğunu belirtti.

Ek Deneyler ve Verimlilik Bulguları

Anthropic, OSS-Fuzz’ın yanı sıra Claude’dan zlib sıkıştırma biçimini tanımlayan teknik belge RFC 1950 için biçimsel bir belirtim yazmasını ve ardından Linux çekirdeğinin zlib uygulamasının bu belirtimi doğru biçimde uyguladığını kanıtlamasını istedi. Claude, x86 komut kümesinin Claude tarafından oluşturulan biçimsel semantiklerini kullanarak x86 için derlenmiş ikili dosyayı doğrudan kanıtladı. Anthropic, bu süreci yaygın olarak kullanılan yarım düzine başka kütüphane için de tekrarladığını ve küçük, istismar edilemeyen uç durum hataları bulduğunu; bu hataların üst projelere bildirildiğini söyledi. Şirket ayrıca x86 semantiklerinin oluşturulması sırasında resmî başvuru belgelerinde yüzlerce hata ve donanımın kendisinde daha az sayıda hata tespit edildiğini; semantik adım adım yürütüldüğünde Linux çekirdeği üzerinde Ubuntu kullanıcı alanının başlatılabildiğini bildirdi.

Başka bir deneyde Claude, Rust ile Python’ın büyük bir alt kümesi için bir yorumlayıcı geliştirdi ve Verus doğrulama aracını kullanarak yorumlayıcının akademik bir makalede açıklanan CPython semantiğine uyduğunu kanıtladı. Teknik ekte, yorumlayıcının 17 katmanının tamamının kanıtlandığı ve şu teoremin geçerli olduğu belirtiliyor: “Yorumlayıcı bir sonuç döndürdüğünde, bu sonuç biçimsel semantiğin öngördüğü sonuçtur.” Anthropic, rastgele oluşturulmuş 1,7 milyon Python programı üzerinde yapılan deneysel testlerde, testlerin %99,95’inde davranışın CPython ile aynı bulunduğunu söyledi. Kasıtlı olarak enjekte edilen yedi hatadan beşi rastgele testlerden sağ çıkarken, yedisi de kanıtı geçersiz kıldı.

Anthropic, verimliliği ölçmek için gerçek OSS-Fuzz giriş noktalarını küçülterek 36 küçük doğrulama görevi oluşturdu. Böylece, girdileri 64 baytla sınırlı ve yaklaşık 100 komutluk bir “mini-ASan” çalışma zamanı kullanılan; AddressSanitizer’ın yerini bu çalışma zamanının aldığı, 283–2.491 komut uzunluğunda programlar elde etti. Anthropic’in bildirdiğine göre Opus 5.5, görevlerin yarısını Opus 5’e kıyasla yaklaşık %40 daha az token kullanarak kanıtlıyor. Anthropic ayrıca, ortak bir çalışma alanında birbirlerinin kanıtlarını kopyalamalarına izin verilen ajanların tek başına çalışan ajanlardan %17 daha az token kullandığını, bazılarının tek başlarına çalışırken başarısız olduktan sonra görevi tamamladığını ve tek başına çalışan ajanların iki kanıtı tamamlayamadığını bildirdi. Şirket, OSS-Fuzz çalışması sırasında da bu yeniden kullanım etkisinin büyük ölçekte görüldüğünü söyledi: Her kanıtın önemli bir bölümü ortak C çalışma zamanı ve AddressSanitizer başlatma kodunu kapsadığı için ajan ekipleri tamamlanmış kanıtları kopyalayıp uyarladı.

Belirtilen Sınırlamalar ve OSS Verify Programı

Anthropic, bu kanıtların kütüphanelerin hatasız olduğu anlamına gelmediğini belirtiyor: Kalan hatalar, güvenilen bileşenlerde veya kanıtların kapsamı dışında bulunabilir. Kanıtlar, musl libc’ye bağlanan tek iş parçacıklı statik RISC-V ikili dosyalarını kapsıyor. Oysa çoğu kullanıcı bu kütüphaneleri x86 veya ARM üzerinde çalıştırıyor ve glibc’ye dinamik olarak bağlıyor; ayrıca AddressSanitizer bellek güvenliğiyle ilgili tüm hataları tespit etmiyor. Şirket, modeller geliştikçe bu sınırlamaların aşılabilir hâle gelmesini beklediğini söyledi.

Theorem, uygun nitelikleri taşıyan açık kaynaklı projelere aynı işlem hattını OSS Verify programı aracılığıyla ücretsiz sunuyor. Programa katılmak için proje deposuna project.yaml, Dockerfile ve build.sh dosyalarını ekleyen bir çekme isteği göndermek gerekiyor. Theorem, projeleri OSS-Fuzz’a benzer ölçütlerle değerlendirdiğini ve yaygın olarak kullanılan kritik altyapılara öncelik verdiğini söylüyor. Theorem’e göre geliştiriciler, her bir fuzz hedefinin 64 MiB’a kadar olan hiçbir girdide çökmeyeceğini gösteren ve Rocq çekirdeği tarafından denetlenen bir Rocq kanıtı alıyor. Kanıt çalışması sırasında bulunan hatalar, herhangi bir açıklama son tarihi olmaksızın, e-posta yoluyla özel olarak geliştiricilere bildiriliyor; kanıtların üretilmesi birkaç gün sürebiliyor. Theorem’in yol haritasında, glibc, OpenSSL ve cURL gibi kritik altyapılar da dâhil olmak üzere Nix ekosisteminin tamamının doğrulanması hedefleniyor.