Anthropic: Claude telah diverifikasi secara formal dalam skala besar untuk perpustakaan open-source

Pada 22 Oktober, Frontier Red Team milik perusahaan kecerdasan buatan Anthropic merilis sebuah penelitian yang menyatakan bahwa model bahasa besar (LLM) kini telah mampu menghasilkan bukti formal secara otomatis dalam skala yang jauh lebih luas. Tim ini berkolaborasi dengan Theorem untuk melakukan verifikasi formal terhadap sifat keamanan lebih dari 100 pustaka sumber terbuka nyata—pada tingkat kode mesin RISC-V—menggunakan model Claude. Ini merupakan verifikasi formal berskala besar pertama yang dilakukan oleh sistem AI terhadap perangkat lunak tingkat produksi pada level kode mesin. Selama proses pembuatan bukti, tim juga secara tak terduga menemukan sejumlah celah keamanan yang telah lama tidak terdeteksi. Metode eksperimen melibatkan konversi kasus uji fuzz yang dapat dikompilasi dari Google OSS-Fuzz menjadi spesifikasi formal, lalu menjalankan verifikasi terhadap input berukuran maksimal 64 MB—dalam kondisi terbatas seperti eksekusi tunggal (single-thread), biner statis, anggaran memori tetap, arsitektur CPU RISC-V, serta lingkungan runtime Linux.