Claude Buktikan 239 Library Open Source Tak Bisa Crash

Bayangkan kamu menguji kekuatan jembatan dengan mengirim sejuta mobil melewatinya setiap hari. Kalau tidak ada yang runtuh, kamu merasa jembatan itu kuat. Tapi kamu tidak pernah tahu pasti apakah mobil ke satu juta satu akan membuatnya ambruk.

Begitulah cara industri software menguji keamanan selama ini: fuzzing, melempar jutaan input acak dan berharap menemukan yang bikin crash. Pada 22 Oktober 2026, tim riset Anthropic yang berkolaborasi dengan startup Theorem mengumumkan sesuatu yang jauh lebih berani. Mereka memakai Claude untuk membuktikan secara matematis bahwa 239 titik masuk di 123 library open source tidak akan pernah crash.

Bukan sekadar menemukan bug, melainkan membuktikan ketidakberadaan bug. Perbedaannya besar, dan inilah cerita di baliknya. Kalau pendekatan ini berhasil diskalakan, cara kita menulis software yang aman bisa berubah total.

Apa yang Sebenarnya Dibuktikan Claude?

Claude mengambil pendekatan yang tidak biasa. Ia tidak membaca source code, melainkan bekerja di level biner yang sudah dikompilasi menjadi instruksi RISC-V. Dari biner inilah ia membangun model matematis tentang perilaku program.

Untuk setiap titik masuk fuzz test dari proyek Google OSS-Fuzz, Claude menulis bukti formal dengan satu klaim sederhana: program ini tidak akan pernah crash untuk semua input di bawah 64 MB, di setiap respons sistem operasi Linux dan tata letak memori yang dimodelkan. Kalau bukti itu lolos, fuzzing di titik masuk tersebut jadi tidak diperlukan lagi.

Buktinya ditulis dalam bahasa Rocq, lalu diperiksa oleh kernel Rocq yang independen. Kamu tidak perlu membaca buktinya baris demi baris. Yang perlu kamu percayai hanya tiga hal: model formal RISC-V dan proses Linux, pernyataan teorema yang dibuktikan, dan pemeriksa Rocq itu sendiri.

180 Juta Baris Bukti Matematika

Skalanya sulit dibayangkan. Total bukti yang ditulis Claude mencapai sekitar 180 juta baris Rocq. Bukti tipikalnya saja sekitar 600 ribu baris, hanya untuk mengamankan biner dengan panjang median 18 ribu instruksi RISC-V. Butuh waktu beberapa minggu bagi Claude untuk menambal bug yang ia temukan, lalu menyelesaikan pembuktian seluruh 239 titik masuk.

Kabar baiknya, model yang lebih baru makin hemat. Pada 36 tugas verifikasi kecil, Claude Opus 5.5 berhasil membuktikan separuhnya dengan sekitar 40 persen token lebih sedikit dibanding Opus 5. Tren efisiensi ini diperkirakan terus berlanjut seiring model dilatih pada tugas verifikasi yang panjang.

Bukti-bukti ini juga bisa dipakai ulang. Sebagian besar bukti menyangkut kode yang dimiliki semua program, seperti inisialisasi runtime C dan AddressSanitizer. Ketika agen-agen Claude saling menyalin bukti yang sudah jadi lalu mengadaptasinya, mereka butuh 17 persen token lebih sedikit dibanding bekerja sendiri.

Bug Lama yang Akhirnya Ketangkap

Justru dalam proses membuktikan inilah Claude menemukan ratusan bug yang lolos dari pengujian bertahun-tahun. Contohnya counter underflow di sebuah decompressor yang menyebabkan out-of-bounds write, tapi hanya muncul pada input sekitar 20 MB dengan tata letak yang sangat langka. Fuzzer biasa tidak akan pernah menyentuhnya.

Ada juga out-of-bounds read di image decoder yang butuh input 64 MB plus memori lebih dari 2 GB, serta penemuan ulang CVE-2026-56132 di libexpat lewat input yang bersarang dalam. Bahkan bug logika yang tidak pernah crash pun ketahuan, misalnya fitur pembatas file yang boleh dimuat ternyata tidak selalu ditegakkan.

Claude juga membuktikan implementasi zlib di kernel Linux benar-benar sesuai RFC 1950, kali ini langsung di biner x86. Dan saat mencoba memverifikasi PDF reader yang populer, ia menemukan bug keamanan sebanyak laporan setahun penuh hanya dalam waktu satu minggu.

Semua Bukti Dirilis Terbuka

Anthropic tidak menyimpan hasilnya sendiri. Mereka merilis subset bukti lengkap beserta semantik formal RISC-V dan sistem operasi di GitHub, supaya siapa pun bisa memverifikasi ulang dan menggunakannya kembali. Bukti yang berpotensi membocorkan bug yang belum ditambal memang sengaja tidak dirilis.

Theorem, startup yang berkolaborasi dalam riset ini, juga merilis Claude skill untuk membantu developer memverifikasi kode mereka sendiri. Rilis terbuka ini penting karena bukti yang bisa diverifikasi ulang jauh lebih meyakinkan daripada klaim sepihak. Mereka bahkan punya peta jalan ambisius: memverifikasi seluruh ekosistem Nix, termasuk infrastruktur kritis seperti glibc, OpenSSL, dan cURL.

Apakah Ini Berarti Bebas Bug?

Anthropic sendiri menegaskan satu hal penting: formally verified tidak sama dengan bug-free. Buktinya hanya berlaku untuk biner statis single-thread di CPU RISC-V yang memakai musl libc, sementara kebanyakan orang menjalankan library ini di x86 atau ARM dengan glibc. AddressSanitizer pun tidak mendeteksi semua bug memory safety, dan tidak semua titik masuk berhasil dibuktikan.

Tapi peta jalannya jelas. Verifikasi formal yang dulu butuh puluhan tahun kerja ahli kini bisa diskalakan oleh LLM, dan suatu hari akan sepraktis fuzzing. Kalau kamu penasaran dengan eksperimen semacam ini, mampir ke /projects untuk melihat proyek yang pernah aku bangun.