AI akan Membuat Verifikasi Formal Menjadi Arus Utama
(martin.kleppmann.com)- Verifikasi formal (formal verification) adalah metode untuk membuktikan secara matematis bahwa kode selalu memenuhi spesifikasi, dan selama ini lama bertahan di ranah yang terbatas serta berpusat pada riset
- Beberapa sistem besar seperti mikrokernel seL4 telah dikembangkan dengan verifikasi formal, tetapi karena tingkat kesulitan dan biaya yang tinggi, metode ini hampir tidak digunakan di lingkungan industri
- Baru-baru ini, alat bantu coding berbasis LLM menunjukkan hasil tidak hanya pada kode implementasi tetapi juga dalam penulisan skrip pembuktian di berbagai bahasa, sehingga muncul kemungkinan untuk mengubah struktur biaya verifikasi secara besar-besaran
- Jika AI dapat mengotomatisasi pembuktian kebenaran sekaligus pembuatan kode, pengembangan perangkat lunak dapat beralih ke pendekatan yang lebih dapat dipercaya daripada code review manusia
- Otomatisasi verifikasi formal adalah teknologi kunci untuk memastikan keandalan perangkat lunak di era AI, dan hambatan utama untuk menjadi arus utama tampaknya lebih berupa perubahan budaya daripada keterbatasan teknis
Kondisi Saat Ini dan Batasan Verifikasi Formal
- Bahasa dan alat berorientasi pembuktian seperti Rocq, Isabelle, Lean, F*, Agda memungkinkan pembuktian matematis bahwa kode memenuhi spesifikasi
- Contoh representatifnya meliputi kernel sistem operasi seL4, kompiler C CompCert, dan stack protokol kriptografi Project Everest
- Namun, di lingkungan industri verifikasi formal hampir tidak digunakan
- Dalam kasus seL4, memverifikasi 8.700 baris kode C memerlukan 20 person-year dan 200.000 baris kode Isabelle
- Untuk setiap satu baris implementasi, dibutuhkan 23 baris pembuktian dan setengah hari kerja manusia
- Secara global, jumlah ahli yang mampu menulis pembuktian semacam ini diperkirakan hanya ratusan orang
- Dari sisi ekonomi juga, pada sebagian besar sistem biaya verifikasi lebih besar daripada kerugian akibat bug, sehingga nilai praktisnya rendah
Bagaimana AI Mengubah Ekonomi Verifikasi Formal
- Baru-baru ini, asisten coding berbasis LLM menunjukkan hasil bukan hanya pada kode implementasi tetapi juga pada penulisan skrip pembuktian
- Nature, Galois, arXiv, dan lainnya melaporkan kasus LLM yang menghasilkan pembuktian dalam berbagai bahasa
- Saat ini masih diperlukan bimbingan ahli, tetapi otomatisasi penuh diperkirakan mungkin terjadi dalam beberapa tahun ke depan
- Jika biaya verifikasi turun drastis, verifikasi formal dapat diterapkan pada lebih banyak perangkat lunak
- Pada saat yang sama, kode yang dihasilkan AI memerlukan verifikasi formal untuk menjamin keandalan sebagai pengganti peninjauan manusia
- Jika AI dapat membuktikan sendiri kebenaran kodenya, pendekatan ini berpotensi lebih disukai daripada kode yang ditulis manual
Saling Melengkapi antara LLM dan Verifikasi Pembuktian
- Saat LLM menulis skrip pembuktian, walaupun menghasilkan isi palsu (halusinasi), proof checker akan menolaknya
- Checker disusun dari basis kode kecil yang telah diverifikasi, sehingga sulit bagi pembuktian yang salah untuk lolos
- Karena itu, ketidakpastian LLM dapat dilengkapi oleh ketelitian verifikasi formal
- Kombinasi ini berfungsi sebagai jalur otomatisasi yang aman untuk menjamin keandalan kode yang dihasilkan AI
Tantangan Baru: Ketepatan dalam Mendefinisikan Spesifikasi
- Bahkan dalam lingkungan verifikasi otomatis, mendefinisikan spesifikasi (specification) dengan benar tetap menjadi tantangan utama
- Perlu dipastikan bahwa properti yang dibuktikan benar-benar sesuai dengan properti yang dimaksud pengembang
- Penulisan spesifikasi tetap memerlukan keahlian dan pemikiran yang cermat, tetapi jauh lebih sederhana dan cepat daripada pembuktian manual
- AI juga dapat mendukung penerjemahan spesifikasi antara bahasa alami dan bahasa formal
- Namun, ada risiko kehilangan makna, meski ini dinilai masih berada pada tingkat yang dapat dikelola
Prospek Perubahan dalam Cara Pengembangan Perangkat Lunak
- Pengembang dapat beralih ke bentuk kerja di mana properti kode yang diinginkan dituliskan sebagai spesifikasi deklaratif, lalu AI menghasilkan implementasi dan pembuktian sekaligus
- Dalam skenario ini, pengembang tidak perlu meninjau langsung kode yang dihasilkan AI, dan dapat menggunakannya berdasarkan kepercayaan seperti pada bahasa mesin dari compiler
- Singkatnya, tiga perubahan berikut diperkirakan akan terjadi
- Penurunan tajam biaya verifikasi formal
- Peningkatan kebutuhan verifikasi untuk memastikan keandalan kode buatan AI
- Ketelitian verifikasi formal melengkapi sifat probabilistik LLM
- Jika faktor-faktor ini berpadu, verifikasi formal kemungkinan besar akan menjadi teknologi arus utama dalam rekayasa perangkat lunak
- Ke depan, faktor pembatasnya diperkirakan bukan teknologi, melainkan kecepatan penerimaan perubahan budaya pengembangan
1 komentar
Komentar Hacker News
Saya rasa verifikasi formal (formal verification) benar-benar menunjukkan nilainya di bidang yang implementasinya jauh lebih kompleks daripada spesifikasinya
Contohnya seperti optimisasi tingkat bit pada implementasi kriptografi atau tahap optimisasi compiler
Namun, karena kode yang ditulis sebagian besar developer (atau AI) sudah dekat dengan spesifikasi berkat bahasa tingkat tinggi, saya rasa manfaat verifikasi formal tidak terlalu besar
Saya juga ragu menulis spesifikasi secara terpisah akan lebih mudah dibaca
Bahkan sekarang pun berbagai framework dan library sudah mengabstraksikan detail implementasi
Verifikasi formal memang bisa memberi jaminan yang lebih kuat, tetapi kebanyakan orang tidak menginginkan tingkat jaminan seperti itu, dan saya rasa AI juga tidak akan menciptakan kebutuhan baru akan hal tersebut
Beberapa orang memprediksi AI akan sepenuhnya mengotomatiskan verifikasi formal, tetapi saya melihat ada masalah dalam logika itu
Jika AI bisa membuktikan perangkat lunak secara otomatis, maka tidak perlu lagi memverifikasi perangkat lunak yang ditulis manusia
AI akan bisa merancang ide, mengimplementasikannya, dan menentukan tingkat verifikasi sendiri
Pada akhirnya, pemrograman atau verifikasi yang dilakukan manusia kemungkinan besar akan hilang
Manusia memang bisa merancang proof assistant, tetapi menggunakan itu untuk memverifikasi program besar jauh lebih sulit
Jadi jika AI semacam itu muncul, ia kemungkinan juga akan bisa membuat proof assistant baru sendiri
Tentu saja, bayangan seperti ini lebih dekat ke wilayah fiksi ilmiah dan tidak ada gunanya membuat prediksi saat kita bahkan belum tahu dengan jelas pekerjaan apa yang akan dibuat AI menjadi lebih mudah atau lebih sulit
Tautan diskusi terkait
Rasanya itu akan menjadi titik balik ketika umat manusia masuk ke fase yang benar-benar berbeda
Untuk mendapatkan hasil yang berguna dari coding agent (Claude Code, Codex CLI, dll.), kuncinya adalah menyiapkan lingkungan untuk menjalankan dan memverifikasi kode yang mereka tulis dengan baik
Bahasa seperti Python paling cocok karena mudah dijalankan, dan untuk HTML+JS kita perlu alat seperti Playwright
Tahap berikutnya adalah test suite otomatis, lalu alat kualitas seperti formatter kode, linter, dan fuzzer
Debugger juga bagus, tetapi karena bersifat interaktif, agent jadi sulit menanganinya
Saya rasa alat verifikasi formal juga termasuk dalam spektrum ini — karena model belakangan ini juga cukup mahir menangani bahasa pemrograman khusus
Jika Anda merasa coding agent tidak terlalu berguna, kemungkinan besar penyebabnya adalah kurangnya lingkungan eksekusi dan pengujian
Ambil Haskell sebagai contoh, jika sudah berhasil dikompilasi, hampir selalu berjalan dengan benar
Jika sifat seperti ini berguna bagi manusia, maka hal yang sama juga berlaku untuk LLM
Terutama property test sangat cocok dengan LLM — karena dengan sedikit pengujian bisa mencakup area kesalahan yang luas
Melihat ada upaya di komunitas matematika untuk memakai LLM dalam meningkatkan kode Lean, rasanya pengembangan perangkat lunak dengan memanfaatkan sistem tipe yang lebih kuat juga sangat mungkin dilakukan
Debugging tidak bersifat sekuensial, dan waktu sebab serta akibat sering tercampur
Dulu saya pernah mencoba ChatGPT saat memburu bug multithread dengan gdb, tetapi yang diulang hanya saran sederhana untuk menambah print
Pada akhirnya saya kembali merasa ini adalah bidang yang membutuhkan pengalaman dan intuisi
Tidak masuk akal menyuruh engineer junior bekerja tanpa debugger atau test runner
Pada akhirnya, sepertinya sumber daya komputasi akan dibutuhkan lebih banyak
Claude mengimplementasikan, lalu Codex dan Gemini melakukan review
Cara ini memang mahal, tetapi sejauh ini menjadi metode paling pasti untuk mengurangi bias diri (self-bias) dan meningkatkan kualitas kode
Alat analisis statis mungkin bisa memberi bantuan tambahan, tetapi rasanya sekadar menambah jumlah tool saja tidak cukup
Jika proses verifikasi diotomatisasi, bagian yang benar-benar sulit akan bergeser ke mendefinisikan spesifikasi secara akurat
Menulis spesifikasi jauh lebih cepat dan mudah daripada pembuktiannya sendiri, tetapi tetap membutuhkan keahlian dan kehati-hatian
Alasan bukti formal dulu tidak menyebar luas bukan hanya karena sulit, tetapi juga karena metode waterfall menghilang dan pengembangan agile menjadi arus utama
Alih-alih menulis spesifikasi panjang, cara kerja berkembang menjadi iterasi cepat yang menyesuaikan dengan kebutuhan pengguna
Sepertinya sekarang saatnya belajar OCaml
Banyak proof assistant dan sistem verifikasi bisa menghasilkan kode OCaml, dan ADA/Spark juga layak dipertimbangkan
Bagaimanapun juga, rekayasa perangkat lunak di era AI akan berubah, tetapi kita harus membuat perangkat lunak dengan kualitas lebih tinggi daripada sekarang
Verifikasi formal jelas akan membantu mencapai tujuan itu
Ini masih belum selesai, tetapi saya membagikan proyek eksperimen saya
Di dunia yang kekurangan tulisan yang berpusat pada kode, ini mungkin layak dilihat oleh seseorang yang mencari ide hackathon yang menarik
Tautan proyek py-mcmas
LLM cenderung bagus dalam masalah yang mudah diverifikasi
Karena itu saya membagi pemecahan masalah menjadi tiga tahap
1️⃣ pertama menulis program kondisi sukses
2️⃣ lalu memakai program itu untuk memverifikasi masalah aslinya
3️⃣ terakhir saya memeriksanya sendiri
Pendekatan seperti ini sudah lama saya gunakan, tetapi sekarang model seperti Opus atau GPT-5.2 juga bisa melakukannya dengan baik dalam mode tanpa pengawasan
Tulisan blog terkait
Di bidang yang verifikasinya memakan waktu lama, beban verifikasi manusia justru bisa bertambah
Bisa saja muncul pertanyaan, “siapa yang memverifikasi program verifikasinya?”
Jika LLM juga yang menulis itu, semuanya bisa tampak seperti menara kura-kura tanpa akhir (turtles all the way down)
Yang sulit adalah proses membuat buktinya
Tentu ada pengecualian pada proposisi yang kompleks, tetapi ini sangat membantu mengurangi bug
Meski verifikasi formal menjadi umum, saya rasa bukan berarti semua orang akan memakai Lean atau Isabelle
Justru kemungkinan besar AI akan menyebar dalam bentuk yang menyatu secara alami ke workflow yang ada
Misalnya verifikasi properti di CI, atau tombol “buktikan invariant modul ini” di IDE
Kebanyakan engineer bahkan tidak perlu melihat langsung script pembuktiannya
Yang benar-benar sulit bukanlah membuat LLM menghasilkan bukti, melainkan membuat organisasi mau berinvestasi dalam menulis spesifikasi dan model
Jika AI memudahkan pengajuan dan revisi spesifikasi, verifikasi akan menjadi alat refactoring yang alami seperti test atau linter
Ada juga yang mengeluh bahwa GPT‑5.2 bahkan tidak bisa menghitung dengan benar berapa banyak huruf r dalam “garlic”
Jika memang perlu, cukup minta LLM menulis skrip Python lalu menjalankannya
Itu memang benar, tetapi hanya detail implementasi tokenisasi dan hampir tidak ada hubungannya dengan kegunaan nyata
Hampir tidak ada alasan memakai LLM untuk menghitung jumlah huruf dalam sebuah kata