Anthropic menyatakan Claude menulis bukti formal bahwa 123 pustaka sumber terbuka tidak dapat mengalami crash

Dalam kolaborasi dengan Theorem, Anthropic menyatakan menggunakan Claude untuk membuktikan properti keamanan pada tingkat assembly (RISC-V) di lebih dari 100 pustaka sumber terbuka yang digunakan di dunia nyata. Anthropic menyebutnya sebagai penggunaan AI skala besar pertama untuk memverifikasi perangkat lunak produksi secara formal pada tingkat tersebut.

Menurut Anthropic:

• Yang dibuktikan: untuk 239 titik masuk uji fuzz di 123 pustaka OSS-Fuzz, program selalu keluar secara normal, tanpa kesalahan keamanan memori atau pernyataan yang gagal, untuk setiap masukan di bawah 64 MB. Hal ini berlaku dengan sejumlah asumsi: biner statis berutas tunggal dengan anggaran memori tetap, pada CPU RISC-V yang menjalankan Linux. Bukti-bukti tersebut berjumlah sekitar 180 juta baris Rocq, yang diperiksa oleh pemeriksa bukti Rocq.
• Caranya: uji fuzz yang sudah ada untuk setiap pustaka diubah menjadi spesifikasi ("uji ini tidak pernah mengalami crash"), lalu Claude menulis buktinya dan menambal bug yang ditemukan selama proses. Anthropic menyatakan hal ini menemukan ratusan bug, termasuk bug yang kemungkinan tidak akan dijangkau oleh fuzzer, seperti penulisan di luar batas yang membutuhkan masukan langka berukuran 20 MB, serta penemuan kembali CVE-2026-56132 di libexpat.
• Eksperimen lain: Claude membuktikan bahwa implementasi zlib di kernel Linux sesuai dengan spesifikasi RFC 1950 pada tingkat biner x86, serta membuat interpreter Python dalam Rust yang perilakunya cocok dengan CPython pada 99,95% dari 1,7 juta program acak. Anthropic juga menyatakan bahwa upaya verifikasi formal pada pembaca PDF yang banyak digunakan menemukan sebanyak mungkin bug keamanan dalam satu minggu, sama banyaknya dengan yang biasanya dilaporkan dalam setahun.
• Biaya: pembuktian dapat memerlukan ratusan juta token. Dalam 36 tugas verifikasi kecil, Anthropic menyatakan Opus 5.5 membuktikan setengahnya dengan sekitar 40% lebih sedikit token daripada Opus 5, dan agen yang berbagi bukti membutuhkan 17% lebih sedikit token.

Anthropic menerbitkan sebagian bukti serta semantik RISC-V dan Linux. Theorem menawarkan untuk menjalankan alur kerja yang sama pada proyek sumber terbuka lainnya dan menerbitkan skill Claude untuk memverifikasi kode Anda sendiri. Anthropic mencatat bahwa ini tidak membuktikan pustaka-pustaka tersebut bebas bug: bug yang tersisa akan berada di komponen tepercaya atau di luar cakupan bukti.