hax 0.4 Rilis — Toolkuy

hax 0.4 dirilis 1 Oktober 2026 oleh Cryspen sebagai kerangka verifikasi formal untuk Rust yang menerjemahkan kode menjadi model Lean agar propertinya bisa dibuktikan mesin. Versi ini menjadikan pipeline Charon dan Aeneas sebagai mesin utama backend Lean, memperluas dukungan bahasa Rust termasuk fungsi yang mengembalikan mutable borrow, dan menyederhanakan instalasi menjadi satu perintah cargo install cargo-hax. Versi ini juga menargetkan Lean v4.31.0 yang masih memiliki bug kesahihan yang diketahui.

TL;DR

hax 0.4 dirilis 1 Oktober 2026 oleh Cryspen sebagai kerangka verifikasi formal Rust.
Backend Lean kini memakai pipeline Charon dan Aeneas yang dikembangkan bersama tim Inria.
Dukungan bahasa Rust bertambah, termasuk fungsi yang mengembalikan mutable borrow seperti di OpenMLS.
Instalasi disederhanakan menjadi cargo install cargo-hax dengan berkas konfigurasi tunggal hax.toml.
Versi ini menargetkan Lean v4.31.0 yang punya bug kesahihan diketahui, upgrade direncanakan rilis berikutnya.

Apa Itu hax dan Apa yang Baru di Versi 0.4?

hax adalah alat yang menerjemahkan kode Rust menjadi bentuk yang bisa dibuktikan secara formal, dengan Lean sebagai salah satu backend utamanya. Tujuannya bukan menggantikan test, melainkan menambah lapisan bukti matematis untuk properti yang tidak cukup diuji dengan contoh: kebenaran batas array, invarian struktur data, atau ketiadaan overflow pada jalur tertentu.

Perubahan terbesar di 0.4 adalah pilihan mesin terjemahan. Sejak awal, hax dirancang sebagai alat multi-backend yang menyasar beberapa asisten pembuktian, dan F* lama menjadi pilihan favorit. Backend Lean ditambahkan sepanjang 2025, dan kolaborasi dengan tim Aeneas yang dimulai di Inria mendorong keputusan untuk langsung memakai pipeline Charon dan Aeneas sebagai mesin terjemahan backend Lean.

Pipeline itu sebenarnya sudah tersedia sejak versi 0.3.7, tetapi rilis 0.4 menjadikannya backend Lean utama secara resmi. Dampak konkretnya adalah cakupan Rust yang lebih luas. Pengumuman resmi menyebut fungsi yang mengembalikan mutable borrow sebagai contoh yang sebelumnya ditolak mesin mereka, dengan potongan kode dari OpenMLS, salah satu upaya pembuktian yang sedang berjalan, sebagai ilustrasi.

Menangani mutable borrow bukan pekerjaan sepele. Menerjemahkan pemanggilan seperti penugasan hasil dari sebuah metode yang meminjamkan data secara mutable memerlukan fungsi balik yang disisipkan di akhir masa hidup variabel untuk memperbarui nilai aslinya. Fungsi balik itu harus dihitung dari kode dan ditempatkan di lokasi yang tepat, dan itulah peran terjemahan Aeneas.

Kenapa Pipeline Charon dan Aeneas Penting?

Karena verifikasi formal Rust bukan hanya soal menerjemahkan sintaks. Setiap alat yang memverifikasi Rust harus menangani dependensinya: intrinsic compiler, pustaka core, std, dan alloc. Cara umum adalah menyediakan model tulisan tangan langsung di dalam prover, misalnya di Lean. Menurut tim hax, pendekatan itu rawan salah, sulit diaudit, sulit diperluas, dan terikat backend.

Untuk mengatasinya, mereka mengembangkan pustaka model untuk core yang ditulis dalam Rust. Model itu mudah diperluas, tidak terikat satu backend, dan diuji secara ketat terhadap padanan aslinya di core. Model tersebut bergantung pada sekumpulan kecil primitif yang harus dimodelkan ulang di pustaka tiap backend, sebuah pemisahan yang membuat penambahan backend baru lebih terkelola.

Bagian kedua dari metodologi hax adalah menempatkan spesifikasi bersama kode. Tim hax mendorong penulisan spec langsung di samping kode Rust selama memungkinkan, dan pada rilis ini Aeneas diperluas dengan dukungan awal untuk pola tersebut, meski masih terbatas pada pre dan post condition untuk item mandiri. Manfaatnya jelas: review dan sinkronisasi antara kode dan pembuktian menjadi lebih mudah karena keduanya berdampingan.

Terakhir, mereka memilih mvcgen sebagai titik masuk pembuktian. Alasan yang disebut adalah preferensi memakai alat standar yang didukung komunitas, karena kecepatan pengembangan mvcgen dinilai luar biasa dan sudah dipakai dalam pembuktian berskala besar.

Apa Risiko dan Batasan yang Perlu Diketahui?

Risiko pertama adalah basis kepercayaan yang tidak kosong. hax sendiri bergantung pada alat sumber terbuka seperti Cargo, rustc, Lean, F*, dan Aeneas, serta mengandalkan model Rust primitif dan model core yang harus setia terhadap implementasi rustc. Tim hax menyatakan mereka memitigasi risiko ketidaksesuaian dengan pengujian ketat, tetapi mereka juga jujur bahwa bug bisa ada di kodebase hax maupun dependensinya.

Batasan kedua lebih konkret: hax 0.4 menargetkan Lean v4.31.0, yang memiliki sejumlah bug kesahihan yang diketahui. Artinya, bukti yang dihasilkan di atas versi Lean itu mewarisi risiko tersebut. Tim hax menyatakan upgrade versi Lean direncanakan pada rilis berikutnya, jadi untuk pekerjaan yang sensitif sebaiknya tunggu versi yang sudah memakai Lean lebih baru.

Batasan ketiga adalah soal cakupan. Dukungan awal untuk spec yang ditulis bersama kode masih terbatas pada pre dan post condition untuk item mandiri. Artinya, pola pembuktian yang lebih kaya belum semuanya bisa diekspresikan dengan cara yang disarankan, dan sebagian pekerjaan masih harus dilakukan dengan pendekatan lama.

Keempat, tim hax menyebut bahwa masalah bisa bersembunyi di seluruh alur kerja, bukan hanya di terjemahan: spec yang salah, kode yang dikecualikan, atau teorema yang diabaikan. Mereka sedang membangun alat untuk menampilkan basis komputasi terpercaya tiap proyek hax, dan itu sendiri menandakan bahwa saat ini transparansi tersebut belum otomatis.

Bagaimana Cara Memakai hax 0.4?

Instalasinya kini jauh lebih ringkas daripada versi sebelumnya. Cukup jalankan cargo install cargo-hax, atau pasang lewat distribusi biner yang disediakan. Setelah terpasang, hax mengurus dependensi lain seperti Charon dan Aeneas secara otomatis lewat perintah cargo hax tools, yang mengunduh biner dan mengelola versinya.

Konfigurasi verifikasi kini disimpan di satu berkas tingkat crate bernama hax.toml yang bisa dikelola bersama versi kode. Di berkas itu pengguna bisa mendefinisikan proof scenario, masing-masing dengan backend tertentu, yang menyasar sebagian crate. Menurut pengumuman resminya, pola ini penting untuk verifikasi yang bisa diperluas dan untuk menargetkan properti berbeda dengan backend berbeda.

Kalau kamu ingin mencoba tanpa memasang apa pun, hax juga menyediakan versi daring. Untuk evaluasi serius, langkah paling masuk akal adalah mengambil satu modul kecil dengan invarian jelas, menulis spec-nya, lalu melihat berapa banyak yang bisa dibuktikan otomatis sebelum memutuskan memperluas ke modul lain.

Kapan Verifikasi Formal Rust Layak Dipertimbangkan?

Layak dipertimbangkan ketika biaya kegagalan jauh lebih besar daripada biaya pembuktian, dan ketika properti yang ingin dijamin bisa dirumuskan secara matematis. Untuk kode yang bug-nya mudah ditemukan lewat test dan dampaknya kecil, verifikasi formal hampir selalu berlebihan.

Pendekatan	Yang dijamin	Biaya	Cocok untuk
Test dan fuzzing	Perilaku benar pada contoh yang diuji	Rendah sampai sedang	Sebagian besar kode aplikasi
Review manual	Kualitas dan niat kode, terbatas pada perhatian reviewer	Sedang	Perubahan yang butuh penilaian desain
Verifikasi formal dengan hax	Properti yang dirumuskan berlaku untuk semua masukan	Tinggi, butuh keahlian	Kode kriptografi, protokol, dan inti keamanan

Kontekstualisasi rilis ini penting: tim hax menyebut lonjakan kemampuan model bahasa dalam menghasilkan pembuktian Lean secara mandiri sebagai pendorong. Kalau biaya menulis pembuktian turun karena sebagian bisa dibantu model, maka ambang di mana verifikasi formal masuk akal ikut bergeser. Namun pergeseran itu bergantung pada toolchain yang matang, dan di situlah rilis seperti hax 0.4 berperan.

Satu hal yang sering dilewatkan: verifikasi formal tidak menghapus kebutuhan memahami sistem. Membuktikan bahwa sebuah fungsi memenuhi spesifikasi tidak berarti spesifikasinya benar. Kesalahan yang paling mahal biasanya justru ada di perumusan properti, bukan di pembuktiannya. Karena itu tim yang memakai hax sebaiknya memperlakukan penulisan spec sebagai pekerjaan desain yang direview seperti kode, bukan sebagai formalitas administratif di akhir proyek.

Apa Rencana Selanjutnya untuk hax?

Rilis berikutnya disebut akan membawa backend ProVerif baru, meningkatkan ketahanan keseluruhan, dan memperbaiki rekayasa pembuktian. ProVerif sendiri adalah alat untuk memverifikasi protokol kriptografi, jadi penambahan backend itu memperluas jenis properti yang bisa diperiksa hax di luar model fungsional yang biasa ditangani Lean.

Alasan strategis di balik arah ini juga menarik. Tim hax menulis bahwa Rust menjadi pilihan populer untuk kode yang ditulis model bahasa, dan Lean sedang mengalami adopsi cepat beserta investasi perkakas. Kombinasi keduanya membuat pipeline Rust ke Lean berpotensi berperan penting dalam meningkatkan kepercayaan pada banyak kodebase kritis, terutama yang kian sering dihasilkan mesin.

Ada ironi yang perlu dicatat. Model bahasa kini bisa menghasilkan pengembangan Lean berskala besar secara mandiri, misalnya untuk solusi Navier-Stokes atau pembuktian teorema terakhir Fermat. Menurut tim hax, aliran pekerjaan pembuktian yang dulu sempit berpotensi membuka menjadi sungai yang deras, dan tantangannya adalah menyalurkan aliran itu ke cara yang berguna, yaitu membuat toolchain verifikasi formal beradaptasi dan membaik.

Untuk pengguna praktis, implikasinya sederhana: pantau rilis berikutnya, terutama kalau kamu memakai Lean v4.31.0 dan peduli pada bug kesahihan yang diketahui. Sampai upgrade versi Lean mendarat, hasil pembuktian dari rilis ini sebaiknya diperlakukan sebagai bukti tingkat riset, bukan jaminan mutlak untuk kode produksi yang sangat sensitif.

FAQ

Apakah hax menggantikan test unit?

Tidak. hax menambah bukti formal untuk properti yang tidak cukup diuji dengan contoh, tetapi test tetap dibutuhkan untuk menangkap kesalahan spesifikasi, kesalahan integrasi, dan perilaku yang tidak dirumuskan dalam properti formal.

Bahasa apa saja yang didukung hax?

Fokus utamanya adalah Rust. hax menerjemahkan kode Rust ke backend pembuktian seperti Lean, dan rilis 0.4 memperluas cakupan bahasa yang didukung, termasuk fungsi yang mengembalikan mutable borrow.

Apakah hax bisa dipakai tanpa memasang Lean secara manual?

Ya. Setelah memasang cargo-hax, perintah cargo hax tools mengurus pengunduhan dan pengelolaan versi dependensi seperti Charon dan Aeneas, sehingga pengguna tidak perlu memasangnya sendiri satu per satu.

Apa fungsi berkas hax.toml?

Berkas itu menyimpan seluruh pengaturan verifikasi di tingkat crate dan bisa dikelola bersama versi kode. Di dalamnya pengguna mendefinisikan proof scenario dengan backend tertentu yang menyasar sebagian crate.

Apakah hasil verifikasi hax bisa dipercaya sepenuhnya?

Belum sepenuhnya. hax 0.4 menargetkan Lean v4.31.0 yang punya bug kesahihan diketahui, dan tim hax menyebut bug juga bisa ada di hax maupun dependensinya, sehingga basis kepercayaan perlu dipahami sebelum mengandalkannya.

Sumber utama: pengumuman hax 0.4 di blog Cryspen, repositori hacspec/hax di GitHub, situs resmi Lean, dan repositori Aeneas.