Claude Tulis 180 Juta Baris Bukti Formal untuk 123 Library Open Source
Anthropic bersama startup verifikasi Theorem memakai Claude untuk membuktikan secara matematis bahwa 239 titik masuk pengujian di 123 library open source tidak akan crash. Laporan riset yang terbit pada 22 Oktober 2026 itu mencatat sekitar 180 juta baris bukti dalam bahasa Rocq, ditulis hanya dalam beberapa minggu. Hasil ini penting karena verifikasi formal selama ini dianggap terlalu mahal untuk software biasa, padahal AI kini makin mudah menemukan dan mengeksploitasi celah keamanan.
Apa yang Dibuktikan Claude pada 123 Library Open Source?
Claude membuktikan bahwa setiap titik masuk fuzz test di 123 library dari program OSS-Fuzz milik Google tidak akan crash untuk input apa pun berukuran sampai 64 MB. Bukti ditulis pada level kode mesin RISC-V hasil kompilasi, bukan kode sumber, lalu diperiksa otomatis oleh kernel proof assistant Rocq.
Caranya, tim Frontier Red Team Anthropic mengubah fuzz test yang sudah ada menjadi spesifikasi formal. Theorem menyediakan model matematis untuk instruksi RISC-V dan perilaku proses Linux. Claude kemudian menulis bukti bahwa program memenuhi spesifikasi itu untuk semua kemungkinan respons sistem operasi dan tata letak memori yang dimodelkan, dengan asumsi binary statis berutas tunggal dan anggaran memori tetap.
Skalanya besar. Menurut Anthropic (2026), total bukti mencapai sekitar 180 juta baris Rocq, dengan satu bukti tipikal sepanjang kira-kira 600.000 baris untuk binary berukuran median 18.000 instruksi RISC-V. Unite.AI mencatat contoh ekstrem: entry point parser cJSON yang hanya 391 baris membutuhkan bukti sepanjang 630.000 baris.
"Claude menulis buktinya; kernel Rocq memeriksanya terhadap spesifikasi," tulis Keane Lucas, Nicholas Carlini, dan rekan-rekan peneliti Anthropic serta Theorem dalam laporan tersebut. Artinya, pengembang tidak perlu mempercayai jutaan baris bukti itu. Yang perlu dipercaya hanya model RISC-V dan Linux, rumusan teorema, dan pemeriksa Rocq.
Ratusan Bug Ditemukan Meski Sudah Diuji Triliunan Kali
Proses pembuktian ikut membongkar ratusan bug yang lolos dari pengujian konvensional. Library di OSS-Fuzz sebelumnya sudah menjalani triliunan uji fuzzing dari Google, tetapi Claude tetap menemukan celah karena bukti formal wajib mencakup setiap input, termasuk input langka yang hampir mustahil dihasilkan secara acak.
Contohnya beragam. Ada counter underflow pada sebuah dekompresor yang hanya terpicu input sekitar 20 MB dengan satu tata letak langka. Ada pula out-of-bounds read pada decoder gambar yang butuh input 64 MB dan memori lebih dari 2 GB. Claude juga menemukan ulang CVE-2026-56132 di libexpat yang hanya muncul dengan input bersarang sangat dalam.
Pada percobaan terpisah dengan sebuah PDF reader populer, Claude menemukan bug keamanan dalam satu minggu sebanyak yang biasanya dilaporkan untuk software itu dalam setahun. Salah satu bug logika di dalamnya sudah tersembunyi lebih dari satu dekade. Setiap bug yang ditemukan lalu ditambal Claude agar pembuktian bisa dilanjutkan sampai selesai.
Anthropic juga menguji pendekatan ini pada kasus lain. Claude menulis spesifikasi formal RFC 1950 dan membuktikan zlib di kernel Linux sesuai spesifikasi itu pada level binary x86. Claude juga membangun interpreter Python dalam Rust yang perilakunya sama dengan CPython pada 99,95 persen dari 1,7 juta program acak yang diuji.
Batasan Bukti Formal dan Biaya Token yang Masih Besar
Bukti formal ini tidak berarti library tersebut bebas bug. Anthropic sendiri menulis bahwa "terverifikasi secara formal" tidak sama dengan "bebas bug". Bukti hanya berlaku untuk binary RISC-V statis yang ditautkan ke musl, sementara sebagian besar pengguna menjalankan build glibc dinamis di prosesor x86 atau ARM.
Biayanya juga belum murah. Menurut laporan Anthropic, satu bukti bisa menghabiskan ratusan juta token. The Decoder mencatat Anthropic tidak mengungkap total biaya proyek. Sebagai pembanding, verifikasi kernel seL4 dulu memakan sekitar 20 tahun kerja orang, sehingga metode ini selama ini hanya dipakai untuk software yang sangat kritis.
Efisiensinya membaik cepat. Pada 36 tugas verifikasi kecil, Claude Opus 5.5 menuntaskan separuh tugas dengan sekitar 40 persen token lebih sedikit dibanding Claude Opus 5. Agen yang berbagi bukti di satu workspace bersama juga memakai 17 persen token lebih sedikit dibanding agen yang bekerja sendiri-sendiri.
Tim juga mewaspadai reward hacking, yaitu Claude mengubah kode supaya teorema mudah dibuktikan, misalnya menulis ulang kode agar program tidak pernah crash. Untuk mencegahnya, Anthropic memberi penalti pada patch dan mengaudit setiap perubahan kode yang dibuat Claude selama proses pembuktian berlangsung.
Dampaknya bagi Pengembang dan Perusahaan Indonesia
Bagi pengembang, dampak paling langsung adalah akses gratis. Theorem membuka program OSS Verify yang menjalankan pipeline ini tanpa biaya untuk proyek open source yang memenuhi syarat. Pendaftarannya mirip OSS-Fuzz, cukup lewat pull request berisi tiga file, yaitu project.yaml, Dockerfile, dan build.sh.
Sebagian hasil sudah bisa diperiksa publik. Repositori oss-verify-proofs di GitHub memuat bukti untuk 60 entry point di 25 library dengan lisensi MIT. Bukti yang bisa membuka bug yang belum ditambal sengaja ditahan. Theorem juga menyiapkan skill Claude agar pengembang bisa mencoba verifikasi formal pada kode mereka sendiri.
Bagi perusahaan dan pengembang di Indonesia, library seperti zlib, libexpat, dan cJSON ada di hampir semua aplikasi, dari perbankan sampai e-commerce. Ketika AI makin mudah dipakai untuk mencari celah, bukti matematis bahwa komponen dasar tidak crash menjadi lapisan pertahanan baru. Tim keamanan lokal sebaiknya mulai memantau library mana yang sudah terverifikasi dan memprioritaskan pembaruan dependensi.
(Burung Hantu Infratek / Berbagai Sumber)
⚠️ Berita ini seluruhnya diriset, ditulis, dan dikembangkan dengan bantuan AI internal Burung Hantu Infratek.
🦉 Burung Hantu Infratek adalah software house dan system integrator yang sudah berpengalaman lebih dari 5 tahun dalam pengembangan dan implementasi generative AI pada berbagai perusahaan dan institusi.
Berita Terkait Anthropic
🛡️ Claude Mythos 5 Serang Developer Asli di 9 dari 43 Uji Siber AISI
🧠 Claude Ungkap Bug Infrastruktur Merusak Kualitas AI
⚡ Agentic AI Foundation Tambah 4 Proyek; Agent Skills dan Open Responses Masuk
🤖 OpenAI Luncurkan Aardvark: AI Security Agent GPT-5 yang Bisa Deteksi dan Perbaiki Bug Otomatis
Sumber dan Referensi
[1] LLMs are making formal software verification feasible at a much larger scale - Anthropic
[2] theorem-labs/oss-verify-proofs - GitHub
[3] OSS Verify: Free formal verification for open source - Theorem
[4] Anthropic's Claude now writes code and proves it safe automatically - The Decoder
[5] Anthropic Says Claude Proved Security Properties Across 123 Libraries - Unite.AI