Loading...
Seri: Seri Verifikasi Formal · Bagian 1 dari 3 Audiens: pendatang baru sepenuhnya. Tidak memerlukan latar belakang matematika, pemrograman, atau kriptografi. Apa yang akan Anda dapatkan: pemahaman yang jelas tentang apa artinya membuktikan kebenaran perangkat lunak, mengapa hal tersebut secara fundamental berbeda dari pengujian, apa itu proof yang diperiksa oleh mesin, serta batasan tepat (dan jujur) dari apa yang dapat dijanjikan oleh proof tersebut.
Sebagian besar perangkat lunak dipercaya karena telah diuji: kita menjalankannya pada banyak input dan mengamati perilakunya. Verifikasi formal mengajukan pertanyaan yang lebih berani. Dapatkah kita membuktikan, dengan kepastian matematis, bahwa sebuah sistem melakukan apa yang seharusnya dilakukan untuk setiap input yang memungkinkan, termasuk input yang tidak pernah terpikirkan oleh siapa pun untuk dicoba? Artikel ini membangun ide tersebut dari dasar. Intuisi terlebih dahulu, tanpa simbol hingga Anda layak mendapatkannya.
Ini adalah sebuah kisah nyata, dan inilah alasan mengapa seri ini ada.
Pada tahun 2022, mata uang kripto yang berfokus pada privasi Zcash meluncurkan sebuah pool terlindungi baru bernama Orchard, yang memungkinkan orang untuk bertransaksi dengan jumlah yang tersembunyi. Selama empat tahun, sistem ini berjalan tanpa cela dan lulus audit profesional yang berulang kali dilakukan. Kemudian, pada Mei 2026, seorang peneliti keamanan yang melakukan penalaran secara cermat terhadap matematika yang mendasarinya (dengan bantuan alat AI) menemukan satu titik under-constrained dalam matematika sistem tersebut. Satu celah itu dapat memungkinkan penyerang untuk membuat uang palsu dalam jumlah yang tidak terbatas, dan karena jumlahnya tersembunyi, tidak ada yang akan melihat hal itu terjadi. Celah tersebut telah ada selama ini.
Hal ini tidak terdeteksi oleh pengujian. Setiap pengujian telah berhasil selama empat tahun. Hal ini ditemukan oleh seseorang yang melakukan penalaran terhadap matematika tersebut. Dan ketika tim memperbaikinya, mereka tidak sekadar melakukan patch dan melanjutkan pekerjaan. Mereka menulis sebuah machine-checked mathematical proof, lebih dari 2.700 teorema individu, bahwa penggantinya sama sekali tidak dapat mengandung jenis cacat tersebut.
Itulah verifikasi formal, dan inilah manfaat yang Anda dapatkan: bukan "kami telah mencoba banyak kasus dan semuanya berhasil," melainkan "kami telah membuktikan bahwa hal tersebut berlaku untuk setiap kasus." Untuk sistem di mana satu kasus yang terlewat dapat berakibat katastrofik (uang, pesawat terbang, perangkat medis, kriptografi), perbedaan tersebut adalah segalanya.
Titik buta dalam pengujian telah dinamai beberapa dekade lalu oleh ilmuwan komputer Edsger Dijkstra, dan hal itu masih tetap benar:
Pengujian dapat menunjukkan keberadaan bug, tetapi tidak pernah menunjukkan ketiadaannya.
Jika sebuah pengujian berhasil, Anda telah mempelajari bahwa sistem tersebut berfungsi pada input tersebut. Anda tidak mempelajari apa pun tentang input yang tidak Anda coba, dan bug yang berbahaya hampir selalu berada pada kasus-kasus yang tidak dicoba oleh siapa pun.
Bayangkan Anda bertanggung jawab atas sebuah gedung dengan seribu pintu, dan tugas Anda adalah menjamin setiap pintu terkunci pada malam hari.
Perbedaannya terletak pada antara pengambilan sampel realitas dan pembuktian properti dari sebuah desain. Pengujian melakukan pengambilan sampel. Verifikasi formal memberikan proof. Itulah ide utamanya, dan segala hal lainnya adalah mekanisme untuk melakukannya secara ketat.
Setiap verifikasi formal, tidak peduli seberapa canggihnya, dibangun dari tepat tiga bahan. Pahami hal ini dengan jelas dan sisanya hanyalah detail.
| Pilar | Makna sederhana | Analogi bangunan |
|---|---|---|
| Spesifikasi | Pernyataan tepat tentang apa yang dimaksud dengan "benar" | "Setiap pintu harus dikunci pada malam hari" |
| Sistem | Hal aktual yang sedang diperiksa (sebuah program, sirkuit, protokol) | Bangunan dan mekanisme pengunciannya |
| Proof | Argumen ketat bahwa sistem selalu memenuhi spesifikasi | Demonstrasi logis bahwa menekan "kunci" akan mengunci semua pintu |
Dan bahan keempat yang lebih tenang membuat seluruh hal ini dapat dipercaya:
Proof assistant yang mungkin pernah Anda dengar namanya meliputi Lean, Rocq (sebelumnya Coq), dan Isabelle. Pada dasarnya, mereka adalah mesin pengecek logika yang sangat ketat. Zcash proof dalam cerita pembuka kami ditulis menggunakan Lean. Menariknya, model AI modern semakin banyak digunakan untuk membantu menulis proof ini, dengan manusia sebagai pemandunya, yang telah mempersingkat upaya yang dulunya memakan waktu bertahun-tahun menjadi hanya beberapa minggu. Mesin tersebut tetap memeriksa setiap langkah, sehingga percepatan ini tidak mengorbankan kepastian apa pun.
Kata "proof" mungkin terasa mengintimidasi, jadi mari kita hilangkan kesan misteriusnya dengan contoh konkret yang dapat diperiksa. Tanpa kriptografi, cukup menggunakan aritmatika sekolah.
Klaim: untuk setiap bilangan bulat n, jumlah 0 + 1 + 2 + ... + n sama dengan n(n+1)/2.
Anda dapat mengujinya. n = 5 menghasilkan 0+1+2+3+4+5 = 15, dan 5 × 6 / 2 = 15. ✓ Ini cocok. Coba n = 10: jumlahnya adalah 55, dan formula tersebut memberikan 10 × 11 / 2 = 55. ✓ (Ini dihitung dan dikonfirmasi; klaim tersebut faktanya berlaku untuk setiap n dari 0 hingga 999 saat diperiksa secara langsung.)
Namun menguji nilai-nilai, bahkan hingga ribuan sekalipun, tidak akan pernah mencapai "setiap bilangan bulat." Ada jumlah yang tak terhingga. Sebuah proof menutup celah tak terhingga tersebut dalam argumen yang terbatas, menggunakan teknik yang disebut induksi:
n = 0, jumlahnya hanyalah 0, dan rumus tersebut menghasilkan 0 × 1 / 2 = 0. Keduanya sesuai. ✓k. Sekarang tambahkan angka berikutnya, k+1. Jumlah hingga k+1 adalah (sum up to k) + (k+1) = k(k+1)/2 + (k+1). Satu baris aljabar menyusun ulang ini menjadi (k+1)(k+2)/2, yang merupakan rumus persis dengan k+1 sebagai pengganti k. ✓Karena ia bernilai benar pada awal (0) dan setiap langkah membawanya ke angka berikutnya, maka hal ini berlaku untuk semua bilangan bulat, selamanya, dalam satu argumen yang terbatas. Itulah sebuah proof. Sebuah proof assistant melakukan penalaran yang persis seperti ini, namun memverifikasi secara mekanis bahwa setiap langkah, termasuk "baris aljabar," benar-benar mengikuti apa yang telah dinyatakan sebelumnya.
Lompatan yang layak dipahami: sebuah proof mengubah "kasus yang tak terhingga jumlahnya" menjadi sebuah argumen terbatas yang dapat diperiksa. Itulah kekuatan super yang tidak dimiliki oleh pengujian struktural.
Verifikasi formal sangat kuat sebagian karena adanya wawasan yang memperjelas dari mana bug berasal pada awalnya. Setiap kecacatan dalam sistem pemeriksaan aturan dapat ditelusuri ke salah satu dari tiga tempat:
| Sumber bug | Apa artinya | Bisakah kita membuktikannya agar hilang? |
|---|---|---|
| Spesifikasi | Matematika atau aturan itu sendiri salah (kondisi yang hilang, definisi yang buruk) | Ya, secara langsung, ini adalah bidang utama verifikasi formal |
| Implementasi | Kode gagal menjalankan spesifikasi yang benar dengan setia | Sebagian; sering kali kegagalan semacam itu meninggalkan bukti yang dapat dideteksi |
| Asumsi yang rusak | Sesuatu yang menjadi tumpuan seluruh sistem ternyata salah | Tidak; asumsi adalah fondasi yang tidak dapat dikurangi lagi |
Taksonomi ini lebih penting daripada kelihatannya, dan Bagian 2 serta 3 bergantung padanya. Bug yang paling dalam dan paling berbahaya, jenis yang dapat bersembunyi selamanya, cenderung berada di dalam spesifikasi: deskripsi matematis tentang apa yang seharusnya dilakukan oleh sistem tersebut. Dan spesifikasi adalah tepat apa yang dapat diperiksa secara langsung oleh machine-checked proof, untuk semua kasus sekaligus. Itulah sebabnya upaya verifikasi formal yang serius menargetkan hal tersebut terlebih dahulu.
Verifikasi formal sangatlah kuat, namun janjinya bersifat presisi, dan kesalahpahaman terhadap hal ini dapat menyesatkan orang. Jadi, nyatakanlah dengan hati-hati:
Sebuah proof menjamin bahwa sistem memenuhi spesifikasi, di bawah asumsi yang dinyatakan. Tidak lebih dari itu.
Empat konsekuensi akan menyusul, dan masing-masing sangatlah penting:
Alih-alih memperlemah verifikasi formal, presisi ini justru merupakan kekuatannya. Hal ini memberi tahu Anda dengan tepat apa yang Anda dapatkan. Seperti yang akan kita lihat di Bagian 3, tim Zcash yang menyatakan cakupan dan asumsi mereka secara gamblang ("kami membuktikan soundness supply, di bawah asumsi-asumsi berikut, dan bukan privasi") adalah sebuah model dari kejujuran tersebut.
Untuk menjaga agar teks ini tetap mudah dibaca, kami melakukan penyederhanaan. Spesifikasi yang sebenarnya ditulis dalam bahasa formal yang presisi, bukan dalam kalimat bahasa Inggris; terdapat beberapa gaya verifikasi formal (interactive theorem proving, model checking, metode berbasis SMT) yang sesuai untuk masalah yang berbeda; dan menulis proof ini tetap menjadi pekerjaan yang membutuhkan keahlian serta upaya besar bahkan dengan bantuan AI. Kami juga melewatkan bagaimana sebuah proof assistant merepresentasikan logika secara internal. Semua ini tidak mengubah inti utamanya: sebuah spesifikasi, sebuah sistem, dan sebuah machine-checked proof yang membuktikan bahwa keduanya selaras, di bawah asumsi yang telah dinyatakan. Detail akan kami sertakan kembali saat dibutuhkan.
| Istilah | Makna dalam Bahasa Inggris Sederhana |
|---|---|
| Formal verification | Membuktikan secara matematis bahwa sebuah sistem memenuhi spesifikasi untuk semua kasus |
| Specification | Pernyataan presisi tentang apa yang dimaksud dengan "perilaku yang benar" |
| System | Program, sirkuit, atau protokol aktual yang sedang diperiksa |
| Proof | Rantai langkah logis terbatas yang menetapkan suatu klaim untuk semua kasus |
| Proof assistant / theorem prover | Perangkat lunak (Lean, Rocq, Isabelle) yang memeriksa setiap langkah dari sebuah proof |
| Machine-checked | Diverifikasi langkah demi langkah oleh komputer, bukan hanya melalui pembacaan manusia |
| Induction | Sebuah teknik proof: benar di awal, dan setiap langkah membawanya ke langkah berikutnya |
| Assumption | Sebuah kondisi yang menjadi sandaran proof; jika salah, jaminan tersebut mungkin tidak berlaku |
Apakah verifikasi formal menggantikan pengujian? Tidak. Keduanya saling melengkapi. Pengujian menangkap masalah praktis dan asumsi yang salah dengan biaya murah; verifikasi meniadakan seluruh kelas bug yang mungkin tidak pernah teruji oleh pengujian.
Jika itu begitu kuat, mengapa tidak semuanya diverifikasi secara formal? Hal ini mahal dan membutuhkan keahlian khusus, meskipun bantuan AI sedang menurunkan biaya tersebut. Metode ini dikhususkan untuk sistem di mana bug yang langka dapat berakibat katastrofik, yang mana merupakan kondisi tepat di mana biayanya sebanding dengan hasilnya.
Apakah sistem yang terverifikasi secara formal masih bisa gagal?
Ya, jika spesifikasinya salah, sebuah definisi dinyatakan secara keliru, suatu asumsi tidak terpenuhi, atau kegagalan tersebut berada di luar apa yang telah ditentukan. proof hanya mencakup apa yang diklaim untuk dicakupnya.
Apakah proof yang diperiksa oleh mesin lebih tepercaya daripada proof buatan manusia? Untuk proof yang besar dan rumit, umumnya ya. Sebuah mesin tidak akan melewatkan celah kecil atau menerima penjelasan yang tidak berdasar, meskipun mesin tersebut tetap mempercayai spesifikasi dan definisi yang diberikan kepadanya.
Jika AI membantu menulis proof, mengapa Anda harus mempercayainya? Karena asisten proof memeriksa setiap langkah secara mekanis. AI mengusulkan langkah-langkah; mesin memverifikasinya. Langkah yang salah akan langsung ditolak, sehingga AI mempercepat pekerjaan tanpa memperlemah jaminan tersebut.
Anda membuktikan bahwa perangkat lunak sebuah bank "tidak pernah membiarkan saldo akun menjadi negatif." Setahun kemudian, uang tetap hilang. Bagaimana kedua hal tersebut bisa benar secara bersamaan? (Jawaban di bawah ini.)
proof tersebut menjamin tepat satu properti: saldo tidak pernah menjadi negatif. Dana dapat hilang dengan cara yang tidak pernah ditangani oleh properti tersebut, misalnya bug yang memindahkan dana ke akun yang salah (yang tetap non-negatif), atau cacat pada bagian sistem yang tidak pernah ditentukan. Verifikasi melakukan tepat apa yang dijanjikannya dan tidak lebih dari itu. Ini adalah penerapan peringatan pada Bagian 6: sebuah proof mencakup spesifikasi, bukan setiap gagasan tentang "kebenaran" yang dapat dibayangkan.
Bagian 2 · Bug Orchard: kita beralih ke kisah nyata tahun 2026 secara lengkap. Sebuah sistem privasi menyembunyikan jumlah menggunakan cryptographic proofs, dan satu baris yang kurang terbatasi (under-constrained) dalam matematikanya menyebabkan proofs tersebut dapat dibuat untuk berbohong, sehingga memungkinkan pemalsuan tak terlihat tanpa batas. Kita akan melihat dengan tepat apa yang dimaksud dengan "circuit yang kurang terbatasi", mengapa jenis bug ini dapat tersembunyi selamanya, dan mengapa hal ini telah terjadi lebih dari satu kali.
Bagian dari seri Verifikasi Formal untuk ZecHub.