Google DeepMind Menggunakan Agen AI untuk Memverifikasi Kode Mesin Inti Signal

Google DeepMind memperkenalkan AlphaProof Code pada 10 November 2026, dengan menggunakan tim agen AI untuk menghasilkan bukti Lean yang diperiksa mesin atas properti keamanan tertentu pada kode libsignal hasil kompilasi milik Signal. Tim peneliti yang terdiri atas lima orang menyelesaikan pekerjaan pembuktian dalam empat minggu dan merilis spesifikasi serta artefak verifikasinya untuk ditinjau pihak luar.

Pekerjaan ini melampaui model abstrak desain protokol Signal hingga implementasi hasil kompilasinya. Para peneliti membungkus crate libsignal v0.105.4 dan SPQR v1.6.0 yang tidak dimodifikasi dalam sebuah harness baris perintah sederhana, lalu menggunakan rustc standar untuk membangun executable Linux AArch64 yang ditautkan secara statis. Makalah teknis tersebut menyebut hasil ini sebagai bukti keamanan tingkat protokol pertama untuk kode yang tidak dimodifikasi dari implementasi protokol kriptografi yang digunakan secara luas.

Cara AlphaProof Code Membagi Pekerjaan

Lima peneliti menghabiskan empat minggu untuk mengerjakan pembuktian, menjalankan agen secara terus-menerus di workstation mereka sambil mengembangkan bukti simbolis dan komputasional secara paralel. Makalah tersebut melaporkan bahwa agen menghasilkan sekitar 6,5 juta baris kode bukti Lean yang diperiksa mesin, yang bertumpu pada sekitar 26.000 baris spesifikasi tepercaya dan semantik AArch64.

Manusia memilih properti yang akan dibuktikan, menyelesaikan ambiguitas dan menentukan kompromi keamanan, meninjau spesifikasi, serta memegang persetujuan akhir. Agen yang didukung Gemini 4 Carbon dan Claude Opus 5.5 menyusun dan meninjau spesifikasi tersebut, termasuk peninjauan oleh keluarga model yang berbeda. Tim agen Gemini 4 Carbon kemudian menghasilkan seluruh kode pembuktian; tak satu pun penulis makalah menulis kode pembuktian. Kampanye yang umum menggunakan 40 hingga 80 agen pada satu mesin selama 24 hingga 72 jam. Orkestrator dan ketua tim mengoordinasikan agen pelaksana pembuktian, sementara arsitek dan integrator menjaga basis bukti bersama.

Penjaga gerbang hanya menerima bukti setelah kernel Lean memeriksanya dan sebuah pembanding memastikan bahwa bukti tersebut sesuai dengan spesifikasi yang disisihkan dan disetujui manusia, termasuk setiap definisi transitif, dengan hanya menggunakan aksioma standar Lean. Agen dapat mengusulkan perubahan kecil ketika pembuktian mengungkap masalah dalam spesifikasi, tetapi perubahan pada asumsi tepercaya memerlukan persetujuan manusia atau kebijakan yang ditetapkan pengguna, serta dicatat beserta alasannya. Mekanisme pengendalian ini menangani risiko yang telah didokumentasikan dalam pembuktian yang dihasilkan agen: spesifikasi dapat diperlemah secara tidak langsung melalui salah satu definisinya.

Cakupan Keamanan dan Pengujian Bug Historis

Target yang diverifikasi adalah kode sesi satu-ke-satu yang mencakup jabat tangan PQXDH dan pengiriman pesan Triple Ratchet. Para peneliti melaporkan dua pembuktian independen: sepuluh teorema simbolis berdasarkan asumsi kriptografi ideal dan bukti komputasional yang membatasi keunggulan penyerang melalui asumsi kriptografi dan komponen statistik. Properti yang dicakup meliputi kerahasiaan ke depan, yang melindungi pesan terdahulu setelah keadaan saat ini dicuri; autentikasi; keamanan pascakompromi, yang berkaitan dengan pemulihan setelah kompromi; serta kerahasiaan jabat tangan. Pembuktian simbolis juga mencakup kerahasiaan jabat tangan setelah terjadi pembobolan Diffie–Hellman di kemudian hari.

Untuk menguji apakah spesifikasi tersebut dapat mendeteksi kesalahan nyata, tim membatalkan perbaikan untuk dua bug libsignal yang sebelumnya telah diperbaiki, yang dikenal sebagai weak state dan small subgroup, lalu mengompilasi ulang biner yang telah diubah. Dalam kedua kasus, tim menghasilkan bukti Lean bahwa teorema keamanan simbolis tidak berlaku. Repositori verifikasi publik memisahkan materi komputasional, simbolis, biner bersama, dan semantik AArch64, serta mendokumentasikan cara membangun ulang dan memeriksa bukti secara independen.

Chief Technology Officer Signal, Ehren Kret, mengatakan pekerjaan ini “memberi kami keyakinan yang lebih besar lagi terhadap jaminan privasi dalam kode kami.”

Keterbatasan dan Langkah Selanjutnya

Jaminan ini masih jauh dari sertifikasi untuk seluruh aplikasi Signal. Jaminan tersebut hanya berlaku bagi build libsignal-cli milik para peneliti yang dijalankan sebagai proses baru; pembuatan kunci belum diverifikasi, pengiriman pesan grup ditunda untuk pekerjaan mendatang, sementara kanal samping dan keadaan multi-perangkat berada di luar cakupan skenario ini. Primitif kriptografi tingkat rendah serta rutinitas keluaran dan pustaka tertentu direpresentasikan dengan kontrak tepercaya. Karena itu, hasilnya juga bergantung pada kontrak tersebut, spesifikasi yang disetujui, kernel Lean, semantik AArch64, dan asumsi mengenai primitif yang digunakan.

Makalah tersebut menyatakan bahwa kedua pembuktian tidak membuktikan pemulihan pascakuantum yang dirancang untuk ditambahkan oleh SPQR: teorema komputasional mencakup penyerang klasik, sedangkan teorema ratchet simbolis memungkinkan penyerang memilih kunci SPQR. Model komputasional juga membatasi beberapa tindakan penyerang dan menjadi tidak bermakna pada skala jumlah pesan dan sesi yang cukup besar. Batasan-batasan ini menentukan hal-hal yang harus dipercaya oleh peninjau eksternal sebelum menganggap bukti yang diperiksa mesin sebagai jaminan keamanan untuk penerapan tertentu.

Langkah selanjutnya yang dinyatakan para peneliti adalah memperkuat teorema, mengurangi basis tepercaya dengan memverifikasi lebih banyak rutinitas yang dihubungkan serta mengaitkan kontrak kriptografi dengan implementasi terverifikasi, dan memperluas cakupan ke pengiriman pesan grup, sealed sender, serta protokol sisi server. Tujuan mereka untuk memverifikasi rilis libsignal baru sebelum diluncurkan merupakan sasaran penelitian, bukan penerapan yang telah diumumkan.

Arti penting langsung dari hasil ini terletak pada pembagian tugas yang ditunjukkannya: agen menangani penyusunan bukti, sementara jaminan tetap bertumpu pada spesifikasi yang ditinjau manusia dan asumsi yang dinyatakan secara eksplisit. Publikasi bukti dan prosedur pemeriksaan memberi penelaah eksternal cara untuk menguji landasan tersebut, sementara para peneliti berupaya menerapkan alur kerja ini dalam pengembangan libsignal yang berkelanjutan.