Berita viral dari dunia riset kecerdasan buatan: Anthropic mengumumkan bahwa Claude, bekerja sama dengan perusahaan verifikasi formal Theorem, berhasil membuktikan properti keamanan pada 123 pustaka open source di tingkat kode assembly RISC-V. Bukti yang dihasilkan mencapai sekitar 180 juta baris Rocq. Dalam prosesnya, model menemukan dan menambal ratusan bug yang selama ini lolos dari uji otomatis.
Berita Viral: Kerja Sama Anthropic dan Theorem
Pengumuman itu diterbitkan di halaman riset resmi Anthropic pada 22 Oktober 2026. Tim yang terlibat berasal dari Frontier Red Team, dengan sederet peneliti keamanan dan akademisi sebagai penulis.
Theorem menyediakan semantik formal untuk instruksi RISC-V dan proses Linux. Semantik itulah yang menjadi acuan ketika Claude menulis bukti untuk setiap program yang diuji.
Pendekatannya berbeda dari pengujian biasa. Jika fuzz test hanya menjalankan banyak input dan berharap bug muncul, verifikasi formal berusaha membuktikan tidak ada input yang bisa memicu kesalahan.
Unite.AI merangkum hasilnya: 239 titik masuk fuzz test di 123 pustaka open source, semuanya memperoleh bukti yang diperiksa mesin, bukan diperiksa model yang sama.
Iklan
Campus Commercial Park: rukost di kawasan kampus
C.CO Park menghadirkan kawasan ruko dan kost dalam satu gerbang, dirancang untuk mahasiswa dan penghuni sekitar kampus. Cocok untuk yang mencari aset produktif dengan pengelolaan kawasan yang tertata.
Skala Pekerjaan yang Dihasilkan
Setiap pustaka punya berkas fuzz test yang bisa dikompilasi. Berkas itu diubah menjadi spesifikasi formal yang menyatakan satu aturan sederhana: program tidak boleh gagal untuk input apa pun di bawah 64 MB.
Spesifikasi ditulis pada level instruksi RISC-V hasil kompilasi, bukan pada kode sumber. Karena itu, bukti yang dihasilkan berlaku untuk biner yang benar-benar dijalankan pengguna.
Ukuran bukti jauh melebihi kode aslinya. Satu bukti tipikal mencapai sekitar 600.000 baris Rocq untuk biner dengan panjang median 18.000 instruksi RISC-V.
Totalnya, menurut Unite.AI, Claude menulis sekitar 180 juta baris Rocq dalam proyek ini. Angka itu menjelaskan mengapa pekerjaan ini disebut sebagai penerapan verifikasi formal berskala besar pertama pada perangkat lunak produksi.
Bug yang Tak Terdeteksi Bertahun Tahun
Anthropic menyatakan Claude menemukan bug yang sebelumnya tidak terdeteksi meski pengujian sudah berjalan triliunan kali. Bug itu muncul ketika model mencoba membuktikan aturan keamanan dan gagal di titik tertentu.
Kegagalan membuktikan bukan berarti program pasti salah. Namun pola kegagalan biasanya menunjuk ke bagian kode yang perlu diperiksa lebih teliti, dan di situlah model menemukan masalah.
Setelah menemukan bug, Claude menambal kode lalu mengulang proses pembuktian. Siklus itu berjalan sampai aturan keamanan bisa dibuktikan untuk seluruh rentang input yang diuji.
Anthropic menyebut pendekatan ini mengubah cara kerja pengembangan perangkat lunak. Bug tidak hanya dicari, tetapi juga dinyatakan tidak ada lagi lewat bukti matematis yang bisa diperiksa ulang.
Tiga Komponen yang Masih Harus Dipercaya
Verifikasi formal tidak menghapus kebutuhan akan kepercayaan. Menurut penjelasan Anthropic, ada tiga komponen yang tetap harus dipercaya begitu saja oleh pengguna bukti.
Pertama, model formal dari instruksi RISC-V dan proses Linux. Bila model itu keliru, bukti yang dihasilkan bisa benar secara matematis tetapi tidak mencerminkan mesin sesungguhnya.
Kedua, pernyataan teorema yang dibuktikan. Bila teoremanya terlalu sempit, hasilnya tetap sah tetapi tidak menjawab pertanyaan keamanan yang penting bagi pengguna.
Ketiga, pemeriksa bukti Rocq itu sendiri. Rocq adalah asisten pembuktian yang sudah lama dipakai di lingkungan akademik untuk memeriksa bukti matematis secara mekanis, dan perannya di proyek ini sama.
Batas Klaim yang Perlu Dibaca Cermat
Bukti itu berlaku untuk asumsi tertentu. Program dianggap berjalan sebagai biner statis single thread dengan anggaran memori tetap pada CPU RISC-V yang menjalankan Linux.
Artinya, jaminan bebas crash tidak otomatis berlaku untuk program yang memakai banyak thread, mengakses perangkat keras langsung, atau berjalan di sistem operasi lain.
Anthropic juga menyatakan tidak semua bukti dipublikasikan. Bukti yang berpotensi mengungkap bug yang belum ditambal ditahan lebih dulu agar tidak menjadi petunjuk bagi penyerang.
Klaim bahwa ini upaya berskala besar pertama pada level assembly adalah klaim Anthropic sendiri. Belum ada lembaga independen yang memverifikasi perbandingan dengan proyek verifikasi formal lain.
