Anthropic merilis hasil riset yang cukup ambisius: Claude dipakai untuk membuktikan secara matematis bahwa ratusan program open source tidak akan crash pada kondisi tertentu. Laporannya terbit di blog riset Anthropic dan diumumkan lewat akun X resmi Anthropic pada Jumat (23/10/2026) pukul 05.01 WIB. Proyek ini digarap tim Frontier Red Team Anthropic bersama Theorem, startup yang fokus di verifikasi formal.
Angkanya besar. Claude membuktikan properti keamanan di level kode assembly RISC-V untuk 123 pustaka open source, dan selama proses itu menemukan ratusan bug. Anthropic mengklaim ini sebagai upaya skala besar pertama, sejauh yang mereka ketahui, yang memakai AI untuk menerapkan verifikasi formal pada software produksi di level assembly.
Verifikasi formal sendiri bukan barang baru. Kode diterjemahkan menjadi model matematika, lalu dibuktikan bahwa kode itu selalu mematuhi aturan keamanan tertentu. Masalahnya, cara ini mahal sekali. Anthropic mencontohkan kernel sistem operasi seL4 yang butuh dua person-year untuk dibuat, tetapi 20 person-year untuk diverifikasi.
Bukan Sekadar Uji Coba, tapi Bukti Matematis
Bahan bakunya diambil dari OSS-Fuzz, program Google yang menjalankan fuzz testing terus-menerus untuk proyek open source. Fuzzing bekerja dengan melempar input acak ke program sambil berharap ada yang memicu crash. Di sini, uji fuzz yang ditulis developer diubah menjadi spesifikasi, lalu Claude diminta membuktikan bahwa uji itu tidak akan pernah gagal.
Hasilnya, dalam beberapa minggu Claude menambal bug yang ditemukan lalu membuktikan tidak ada crash untuk input apa pun di bawah 64 MB pada 239 entry point dari 123 pustaka. Pembuktian dilakukan terhadap biner hasil kompilasi, bukan pada kode sumbernya. Bukti ditulis dalam bahasa Rocq dan diperiksa secara mekanis oleh kernel Rocq.
| Aspek | Detail |
|---|---|
| Pustaka OSS-Fuzz yang dibuktikan | 123 |
| Entry point (uji fuzz) yang lolos pembuktian | 239 |
| Batas ukuran input | Semua input di bawah 64 MB |
| Bahasa bukti | Rocq, diperiksa oleh kernel Rocq |
| Total bukti | Sekitar 180 juta baris |
| Ukuran bukti tipikal | Sekitar 600.000 baris |
| Median panjang biner | 18.000 instruksi RISC-V |
| Asumsi lingkungan | Biner statis single-thread, anggaran memori tetap, CPU RISC-V, Linux, musl libc |
| Lama pengerjaan | Beberapa minggu |
Grafik di atas menunjukkan satu trik yang membuat pekerjaan sebesar ini masuk akal. Sebagian besar isi bukti menyangkut kode yang ada di hampir semua program, seperti inisialisasi runtime C dan AddressSanitizer. Tim agen Claude cukup menyalin bukti yang sudah jadi milik program lain, lalu menyesuaikannya.
Ratusan Bug Ketemu di Tengah Jalan
Logikanya sederhana: sesuatu yang salah tidak bisa dibuktikan benar. Setiap kali pembuktian mentok, ada kemungkinan bug di baliknya. Dari situ Anthropic menyebut ratusan bug terungkap, termasuk yang lolos dari fuzzing bertahun-tahun.
Beberapa contohnya cukup spesifik. Ada counter underflow di sebuah decompressor yang berujung pada penulisan di luar batas memori, tetapi hanya muncul pada input sekitar 20 MB dengan susunan langka. Ada juga pembacaan di luar batas memori di decoder gambar yang butuh input 64 MB dan memori lebih dari 2 GB, serta penemuan ulang CVE-2026-56132 di libexpat.
Bug yang tidak bikin crash pun ikut kelihatan. Saat membuktikan sebuah pustaka aman secara memori, Claude mendapati fitur pembatas file yang boleh dimuat aplikasi ternyata tidak selalu ditegakkan. Dalam eksperimen terpisah, upaya verifikasi sebuah PDF reader populer menemukan bug keamanan sebanyak yang biasanya dilaporkan dalam setahun, hanya dalam sepekan.
Anthropic juga mencoba pendekatan lain. Claude membuktikan bahwa implementasi zlib di kernel Linux sesuai spesifikasi RFC 1950, kali ini langsung pada biner x86. Ada pula interpreter Python berbasis Rust yang diverifikasi dengan Verus, lalu diuji dengan lebih dari 1,7 juta program acak dan berperilaku identik dengan CPython pada 99,95 persen tes. Konteksnya relevan, mengingat celah kritis masih terus bermunculan, seperti kasus PHP2Shell yang memaksa PHP merilis patch darurat.
Opus 5.5 Lebih Hemat, Theorem Buka Akses Gratis
Kendala terbesarnya ada di biaya. Satu bukti bisa menghabiskan ratusan juta token. Pada uji 36 tugas verifikasi dari kode OSS-Fuzz, Anthropic menyebut Claude Opus 5.5 menuntaskan separuhnya dengan token sekitar 40 persen lebih sedikit dibanding Opus 5. Saat agen boleh saling menyalin bukti di ruang kerja bersama, kebutuhan token turun 17 persen dibanding bekerja sendiri.
Sebagian bukti dirilis di GitHub Theorem, minus bukti yang bisa membocorkan bug yang belum ditambal. Theorem juga membuka program OSS Verify yang menjalankan pipeline serupa secara gratis untuk proyek open source yang memenuhi syarat. Cara daftarnya mirip OSS-Fuzz, yaitu lewat pull request ke repositori theorem-labs/oss-verify, dan bug yang ditemukan dilaporkan secara privat ke pengelola proyek.
Anthropic sendiri mengakui “terverifikasi formal” tidak sama dengan bebas bug. Buktinya hanya berlaku untuk biner RISC-V statis single-thread dengan musl libc, padahal kebanyakan orang menjalankan pustaka ini di x86 atau ARM dengan glibc. Tidak semua entry point tiap pustaka juga diverifikasi, dan AddressSanitizer tidak menangkap semua jenis bug memori.
Buat pengguna biasa, dampaknya tidak langsung terasa, karena tidak ada aplikasi atau fitur baru yang bisa diunduh. Yang paling diuntungkan adalah pengelola proyek open source, termasuk developer Indonesia yang merawat pustaka C atau C++ dan sudah ikut OSS-Fuzz. Program gratis Theorem layak dicoba oleh mereka. Bagi kami, sisi menariknya ada di arah yang ditunjukkan: kalau biaya token terus turun, verifikasi formal bisa jadi pemeriksaan rutin seperti fuzzing hari ini. Claude Opus 5.5 yang dipakai di riset ini juga menjadi otak Claude Duet, agen AI proaktif yang baru dibuka Anthropic.
