Tanggal artikel: 22 Desember 2025
📝 Deskripsi Ringkas
Artikel ini mengeksplorasi kebangkitan formal verification (verifikasi formal) yang didorong oleh AI, di mana alat bantu bukti (proof assistants) seperti Lean semakin populer. Penulis berpendapat bahwa meskipun verifikasi formal menawarkan jaminan ketidakhadiran bug yang kuat, ia tidak bisa menggantikan pengujian (testing). Sebaliknya, masa depan rekayasa perangkat lunak yang ideal adalah kombinasi sinergis antara verifikasi formal dan pengujian acak (random testing).
1. ⚠️ Problem Statement
Ketiadaan Spesifikasi Formal: Mayoritas perangkat lunak di dunia tidak memiliki spesifikasi formal (deskripsi matematis dari sistem), yang merupakan prasyarat utama untuk verifikasi.
Kesulitan Proof Engineering: Menulis bukti matematika untuk perangkat lunak sangat sulit, membutuhkan keahlian domain spesifik, dan seringkali tidak intuitif bagi insinyur biasa.
Kelemahan Model: Verifikasi formal bergantung pada model sistem. Banyak aspek sistem nyata (seperti performa runtime pada hardware modern dengan cache dan speculative execution) terlalu kompleks untuk dimodelkan secara formal dengan akurat.
Slowness: Kode yang ditulis dalam bahasa pembukti (proof assistants) seringkali sangat lambat (misal: penjumlahan bilangan Peano O(n)) dan tidak praktis untuk beban kerja produksi.
2. 🛠️ Solusi / Approach
Penulis mengusulkan pendekatan jalan tengah:
AI-Assisted Specification: Menggunakan AI untuk membantu menulis spesifikasi formal dari deskripsi verbal, meskipun ini memperkenalkan risiko baru (autoformalization sebagai trusted computing base yang rapuh).
Random Testing sebagai Falsifikasi: Menggunakan pengujian acak (seperti QuickChick) untuk menemukan contoh penyangkal (counterexamples) dengan cepat ketika bukti sulit ditemukan, memberikan umpan balik cepat "jalur salah".
Verification-Guided Development (VGD): Mengimplementasikan dua versi sistem: satu versi sederhana yang diverifikasi formal, dan satu versi produksi yang kompleks dan cepat. Gunakan differential random testing untuk memastikan versi produksi berperilaku sama dengan versi terverifikasi.
3. 📊 Findings / Results / Impact
Keunggulan Verifikasi: Studi kasus CompCert C Compiler menunjukkan keunggulan verifikasi formal; pengujian acak menemukan ratusan bug di GCC dan Clang, namun nol bug di bagian terverifikasi CompCert.
Keterbatasan Verifikasi: Verifikasi tidak bisa membuktikan performa di perangkat keras nyata atau aspek yang tidak dimodelkan.
Sinergi: Pengujian tidak bisa membuktikan ketidakhadiran bug, dan verifikasi tidak bisa memodelkan realitas fisik sepenuhnya. Keduanya saling melengkapi, bukan menggantikan.
4. ⚙️ How to Implement (General Pattern)
Gunakan AI untuk Bukti: Manfaatkan AI coding assistants untuk men-generate bukti formal yang kemudian diperiksa oleh proof checker simbolik (paradigma RLVR).
Terapkan VGD: Jangan coba memverifikasi kode produksi yang sangat teroptimasi secara langsung. Verifikasi model referensi yang sederhana, lalu uji kesesuaian implementasi produksi terhadap model tersebut.
Jangan Tinggalkan Testing: Tetap gunakan pengujian acak untuk memvalidasi asumsi model dan menangkap regresi performa atau perilaku di luar cakupan verifikasi.
5. 💡 Key Takeaways
Trust but Verify (and Test): Janji verifikasi formal yang didukung AI sangat menggoda, tapi jangan tertipu untuk membuang pengujian.
Falsifikasi itu Penting: Mengetahui bahwa teorema Anda salah (melalui tes yang gagal) seringkali lebih berharga daripada berjam-jam mencoba membuktikannya tanpa hasil.
Masa Depan Hibrida: Masa depan perangkat lunak bebas bug bergantung pada integrasi erat antara spesifikasi formal, pembukti otomatis, dan pengujian acak yang kuat.
🗣️ Apakah Anda pernah menggunakan property-based testing (seperti QuickCheck/Hypothesis) dalam proyek Anda? Menurut Anda, apakah itu langkah awal yang baik menuju pola pikir verifikasi formal?
Sumber:
https://alperenkeles.com/posts/test-dont-verify/
🏷️ #FormalVerification #SoftwareTesting #ArtificialIntelligence #SoftwareEngineering #ProofAssistant #Lean #PropertyBasedTesting #VerificationGuidedDevelopment #TechPhilosophy #FutureOfCode
