Frontier Red Team Anthropic merilis riset pada 22 Oktober yang memakai Claude untuk menulis bukti formal bagi 239 titik masuk (entry point) di 123 pustaka open source: selama input lebih kecil dari 64 MB, program-program ini tidak akan crash. Bukti tersebut diletakkan langsung pada berkas eksekusi RISC-V hasil kompilasi, dan mitranya adalah Theorem, perusahaan pembuat perangkat formal. Anthropic menyebut ini pertama kalinya AI melakukan verifikasi formal berskala besar di level assembly pada perangkat lunak produksi.
Seluruh pustaka itu berasal dari proyek OSS-Fuzz milik Google, yaitu kumpulan komponen dasar yang sudah lama berada di platform fuzzing. Kompresi, dekode gambar, dan parsing HTTP termasuk di dalamnya. Seluruh pekerjaan memakan waktu beberapa minggu.
Mengubah uji fuzzing menjadi teorema
Caranya ada tiga langkah. Pertama, tim menulis ulang rangkaian uji fuzz yang sudah dimiliki tiap pustaka menjadi satu spesifikasi formal, yang artinya "kode uji ini tidak akan crash untuk input apa pun". Spesifikasi itu dibangun di atas model semantik instruksi RISC-V dan semantik proses Linux yang disediakan Theorem.
Langkah kedua, Claude menulis buktinya, lalu pemeriksa bukti Rocq memeriksanya baris demi baris.
"Claude writes the proof; the Rocq kernel checks it against the specification."
(Claude menulis bukti, kernel Rocq memeriksanya terhadap spesifikasi.)
Langkah ketiga menangani kasus ketika bukti buntu. Bukti yang macet sering kali menandakan bahwa kode memang mengandung cacat. Saat itu Claude sendiri yang memperbaiki kode, spesifikasi dibuat ulang, lalu pembuktian dilanjutkan. Tim mengakui langkah ini rawan "reward hacking", yakni model bisa mengubah program sembarangan hanya agar bukti lolos. Karena itu mereka memberi penalti pada patch, mewajibkan pembuktian atas rentang input yang terdampak patch, serta mencatat setiap patch untuk diaudit manusia.
Sebuah bukti tipikal berukuran sekitar 600.000 baris. Pada akhirnya, bagian yang perlu dipercaya hanya tinggal model semantik RISC-V dan Linux, pernyataan teorema itu sendiri, dan pemeriksa Rocq.
Bug yang ditemukan selama pembuktian
Ratusan bug ditemukan dan diperbaiki selama pembuktian, sebagian di antaranya sulit ditemukan lewat fuzzing. Artikel itu memberi beberapa contoh: underflow pada penghitung di sebuah dekompresor yang hanya terpicu oleh input tertentu sekitar 20 MB; pembacaan di luar batas pada sebuah dekoder gambar yang baru muncul dengan input 64 MB plus memori lebih dari 2 GB; dan satu pembacaan di luar batas lain yang membutuhkan dua handle mengoperasikan berkas yang sama dalam urutan tertentu. CVE-2026-56132 pada libexpat juga ditemukan kembali.
Pembuktian cpp-httplib punya rintangan tambahan: rekursi saat destruksi std::set bisa menyebabkan stack overflow. Untuk menyingkirkan kemungkinan itu, tim membuktikan di level kode mesin bahwa algoritma penyeimbangan pohon merah-hitam libc++ mampu menjaga kedalaman pohon pada orde logaritmik.
Riset yang sama juga melampirkan beberapa eksperimen sampingan. Claude menulis subset Python dalam Rust dan memakai Verus untuk membuktikan bahwa subset itu sesuai dengan semantik CPython; pada 1,7 juta program acak, perilakunya cocok dengan CPython sebesar 99,95%. Claude juga membuat sendiri satu set semantik instruksi x86 yang dengan eksekusi satu langkah mampu menyalakan userspace Ubuntu, dan sekalian menemukan ratusan kesalahan dalam dokumen referensi resmi.
Bandingkan dengan seL4
Verifikasi formal bukan hal baru di industri; kesulitannya selalu ada pada tenaga manusia. Mikrokernel seL4 kerap dijadikan contoh: sekitar sepuluh ribu baris kode C, dengan upaya pembuktian yang biasanya dikutip sekitar dua puluh orang-tahun. Kompiler CompCert menempuh jalur serupa, dipoles bertahun-tahun oleh tim kecil. Kesamaan proyek semacam ini adalah objeknya sedikit, waktunya panjang, dan butuh banyak pakar.
Skala Anthropic kali ini adalah 123 pustaka dalam beberapa minggu. Jika dibandingkan secara kasar, struktur biaya per satuan pekerjaan sudah berubah bentuk: manusia mundur dari menulis bukti ke menetapkan spesifikasi dan meninjau patch. Biayanya berpindah ke token: artikel menyebut satu bukti lengkap bisa menghabiskan ratusan juta token. Pada 36 tugas kecil, tiap tugas diberi satu agen dengan tiga kali percobaan dan anggaran 5 juta token per percobaan; setelah agen diizinkan memakai ulang bukti satu sama lain, token yang dibutuhkan turun lagi 17%.
Kekuatan jaminannya pun tidak setingkat. seL4 membuktikan kebenaran fungsional, sedangkan kali ini yang dibuktikan hanya "tidak crash", cakupan yang jauh lebih sempit.
Celah di luar bukti
Keterbatasan yang dicantumkan Anthropic sendiri cukup spesifik. Bukti dibangun di atas biner RISC-V single-thread, ditautkan statis, dan memakai musl libc, sedangkan kebanyakan pengguna sebenarnya menjalankan versi x86 atau ARM yang menaut glibc secara dinamis. AddressSanitizer sendiri tidak bisa menangkap semua kesalahan keamanan memori, ada titik masuk yang belum tercakup, dan kerusakan memori akibat pemanggil yang salah memakai pustaka juga berada di luar cakupan bukti.
"Formally verified" does not mean "bug-free."
("Terverifikasi secara formal" tidak berarti "bebas bug".)
Selisih antara spesifikasi dan mesin sungguhan adalah titik yang paling mudah bermasalah pada jalur ini. Rocq dan beberapa model semantik itu sendiri juga perlu diperkuat, dan artikel menyebut hal itu "bukan perkara kecil". Penilaian tim adalah bahwa verifikasi formal akan menjadi tahap rutin dalam pengembangan perangkat lunak yang aman; kapan bukti semacam ini bisa menjangkau lingkungan penerapan arus utama seperti x86 dan glibc, artikel tidak memberikan waktunya.
Sumber: artikel riset Frontier Red Team Anthropic, CocoLoop; halaman riset Anthropic, untuk memeriksa jumlah pustaka, jumlah titik masuk, jumlah baris bukti, dan dasar perbandingan token.