Anda dapat membuktikan kode Rust benar tanpa menulis satu pun bukti. Alat yang melakukannya disebut model checker, dan untuk Rust yang paling praktis saat ini adalah Kani, dibangun oleh AWS. Anda menulis assertion Rust normal. Kani mengubahnya menjadi klaim matematis dan memeriksanya untuk setiap input yang mungkin. Tidak ada theorem prover. Tidak ada proof assistant. Tidak ada penyimpangan enam bulan ke Coq.

Masalahnya adalah “setiap input yang mungkin” hanya berfungsi ketika ruang input cukup kecil untuk dihabiskan. Jika fungsi Anda menerima Vec<u8> dengan satu juta elemen, Kani tidak akan memeriksa setiap permutasi. Ia akan memeriksa hingga batas yang Anda tentukan, atau berjalan hingga laptop Anda kehabisan RAM. Buktinya nyata, tetapi terbatas.

Apa yang sebenarnya dimaksud dengan “bukti tanpa bukti”

Verifikasi formal biasanya berarti menulis program Anda dalam proof assistant seperti Coq, mendefinisikan invariant secara manual, dan membimbing solver melalui langkah-langkah taktis. Compiler terverifikasi seperti CompCert membutuhkan waktu bertahun-tahun. Sebagian besar tim tidak punya waktu bertahun-tahun.

Model checking berbeda. Anda menulis Rust normal. Anda menambahkan fungsi test yang dianotasi dengan #[kani::proof]. Di dalamnya, Anda membuat nilai simbolik dengan kani::any(), memanggil kode Anda, dan membuat assertion. Kani mengompilasi kode Anda menjadi formula logis dan menyerahkannya ke SMT solver. Solver tersebut mengonfirmasi bahwa properti berlaku untuk semua input dalam batas tersebut, atau menghasilkan counterexample yang konkret.

Anda tidak menulis bukti. Anda menulis test dengan kuantor universal. Alat tersebut yang menulis buktinya.

Bagaimana Kani mengubah Rust menjadi logika

Kani adalah bounded model checker. Ia membuka kode Anda menjadi formula logis dan menanyakan kepada SMT solver apakah ada jalur eksekusi yang dapat melanggar assertion. Solver memperlakukan variabel sebagai simbolik. Test normal memberi nilai 5 pada x. Bukti Kani memberikan simbol pada x yang mewakili setiap u32 yang mungkin.

Berikut adalah contoh sederhana. Kita memiliki fungsi yang seharusnya tidak pernah overflow, dan kita ingin membuktikannya.

// src/lib.rs
pub fn saturating_double(x: u32) -> u32 {
    x.saturating_mul(2)
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    fn check_saturating_double_never_overflows() {
        let x: u32 = kani::any();
        let result = saturating_double(x);
        if x > u32::MAX / 2 {
            assert_eq!(result, u32::MAX);
        } else {
            assert_eq!(result, x * 2);
        }
    }
}

Jalankan cargo kani dan Kani memverifikasi ini dalam hitungan detik. Ia memeriksa semua 4.294.967.296 nilai yang mungkin dari x tanpa menjalankannya satu per satu. SMT solver berargumentasi tentang representasi simbolik dan menyimpulkan bahwa tidak ada counterexample yang ada.

Guard #[cfg(kani)] berarti kode ini hanya dikompilasi di bawah Kani. Ia tidak membuat release build Anda membengkak.

Contoh nyata: membuktikan parser bebas crash

Overflow mudah. Kasus yang menarik bergantung pada data. Misalkan kita memiliki fungsi yang mengurai header protocol kecil. Kita ingin membuktikan bahwa ia tidak pernah panic, tidak peduli byte apa yang kita berikan.

// src/protocol.rs
#[derive(Debug, PartialEq)]
pub enum ParseError {
    TooShort,
    InvalidVersion,
}

pub struct Header {
    pub version: u8,
    pub length: u16,
}

/// Parse a 4-byte header:
/// - byte 0: version (must be 1)
/// - byte 1: reserved (ignored)
/// - bytes 2-3: length in big-endian
pub fn parse_header(buf: &[u8]) -> Result<Header, ParseError> {
    if buf.len() < 4 {
        return Err(ParseError::TooShort);
    }
    let version = buf[0];
    if version != 1 {
        return Err(ParseError::InvalidVersion);
    }
    let length = u16::from_be_bytes([buf[2], buf[3]]);
    Ok(Header { version, length })
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    #[kani::unwind(5)]
    fn check_parse_header_no_panic() {
        let len: usize = kani::any();
        kani::assume(len <= 8);
        let buf: [u8; 8] = kani::any();
        let _ = parse_header(&buf[..len]);
    }
}

Kani memverifikasi bahwa parse_header tidak pernah panic untuk setiap buffer input dengan panjang 0 hingga 8. Ia memeriksa test bounds, pemeriksaan versi, dan pengindeksan array. Jika kita menulis buf[1] alih-alih memeriksa panjang terlebih dahulu, Kani akan menemukan counterexample: buffer 1-byte di mana buf[1] berada di luar bounds.

Anotasi #[kani::unwind(5)] memberi tahu Kani berapa kali membuka loop. Karena fungsi kita tidak memiliki loop, ini bersifat konservatif.

Masalah pembatasan: di mana model checking menabrak dinding

Model checking bersifat eksaustif dalam batasannya. Di luar batas tersebut, ia tidak mengatakan apa-apa. Ini adalah trade-off fundamental.

Loop adalah dinding pertama. Kani harus membuka setiap loop sejumlah tetap kali. Jika fungsi Anda mengiterasi Vec dan Anda menetapkan batas unwind ke 10, Kani membuktikan kebenaran untuk vector dengan panjang 0 hingga 10. Ia tidak mengatakan apa-apa tentang panjang 11. Setiap penambahan mengalikan ruang keadaan. Unwind 50 mungkin selesai dalam beberapa menit. Unwind 500 mungkin tidak selesai sama sekali.

Rekursi serupa. Setiap panggilan memperluas formula. Rekursi dalam meledakkan penggunaan memori.

Ukuran data adalah dinding kedua. Kani menangani array dengan ukuran tetap dengan baik. Ia kesulitan dengan koleksi yang dialokasikan secara dinamis kecuali Anda membatasi ukurannya secara eksplisit.

Standard library adalah dinding ketiga. Kani memodelkan banyak di antaranya, tetapi tidak semua. Jika Anda memanggil sesuatu yang tidak dipahami Kani, bukti gagal dengan definisi fungsi yang hilang.

Apa yang dapat dibuktikan Kani dan di mana ia gagal

Kani baik dalam menemukan panic, overflow integer, dan pelanggaran assertion dalam kode terbatas. Ia sangat baik untuk primitif kriptografi, parser protocol, dan state machine kecil. Ini adalah tempat di mana satu input buruk menyebabkan bencana, dan kode secara alami terbatas.

Kani tidak baik dalam membuktikan properti liveness, seperti “setiap request akhirnya mendapat respons.” Itu memerlukan penalaran tentang eksekusi tak terbatas, yang bounded model checking secara eksplisit tidak lakukan. Untuk liveness, Anda ingin temporal model checker seperti TLA+.

Kani juga bukan pengganti test. Bukti yang lulus memberi tahu Anda bahwa tidak ada counterexample dalam batas. Test memberi tahu Anda bahwa kode berperilaku benar untuk input spesifik yang Anda pedulikan. Kani menangkap edge case yang tidak Anda pikirkan. Test menangkap masalah integrasi yang Kani tidak dapat lihat.

Menjalankan Kani di CI tanpa melelehkan runner Anda

Satu bukti Kani pada fungsi kecil membutuhkan waktu detik. Sebuah suite pada crate nyata membutuhkan waktu menit. Bukti dengan batas unwind tinggi dapat memakan waktu berjam-jam. Anda tidak ingin pipeline CI Anda menunggu solve SMT selama dua jam.

Pertahankan bukti Kani tetap kecil dan cepat. Buktikan fungsi safety-critical, yang di mana bug adalah incident. Jangan mencoba membuktikan seluruh web framework Anda. Tetapkan timeout, mungkin lima menit per bukti, dan perlakukan timeout sebagai failure to prove, bukan proof of failure.

Berikut adalah pola Makefile yang berfungsi:

# Makefile
kani:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 300 --all-functions --enable-unstable

kani-fast:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 60 --all-functions --enable-unstable

kani-fast berjalan di CI pada setiap pull request. kani berjalan setiap malam. Jika bukti regresi, Anda mengetahuinya dalam satu hari, bukan setelah shipping.

Jika Anda mengekspos API publik, tulis satu bukti Kani per fungsi publik yang memanggilnya dengan input sepenuhnya simbolik. Ini adalah hal terdekat dengan formal contract test. Ia tidak membuktikan implementasi benar, tetapi membuktikan implementasi tidak crash pada input valid arbitrer.

Kapan menggunakan proof assistant sungguhan

Jika Anda perlu membuktikan properti tentang struktur data tak terbatas, seperti “linked list ini selalu asiklik,” Kani tidak akan membantu Anda. Batas unwind mengalahkan klaim tersebut. Untuk ini, Anda memerlukan alat seperti Creusot, yang menerjemahkan Rust ke WhyML dan menggunakan proof assistant. Ini lebih banyak pekerjaan, tetapi ia menangani struktur tak terbatas.

Jika Anda memerlukan bukti ekuivalensi atau deteksi undefined behavior, alat seperti MIRI atau KLEE berada pada titik yang berbeda pada spektrum effort-versus-coverage. Kani adalah sweet spot untuk “saya memiliki kode terbatas dan ingin tahu apakah ia panic.” Parser, decoder, serializer, dan validator konfigurasi semuanya cocok. Sistem tipe Rust sudah menghilangkan seluruh kelas bug. Kani menghilangkan yang tidak dapat dicapai oleh sistem tipe.

Apa yang dicoba dulu

Jika Anda memiliki crate Rust dengan fungsi yang membuat Anda takut, tambahkan Kani. Fungsi yang menakutkan biasanya adalah yang mengurai untrusted input, melakukan manipulasi bit, atau mengindeks ke array. Tulis proof harness yang memanggilnya dengan kani::any(). Jalankan cargo kani. Jika lulus, Anda memiliki bukti terbatas kebebasan dari crash. Jika gagal, Anda memiliki counterexample konkret yang akan menjadi laporan bug.

Anda tidak perlu mempelajari bahasa baru. Anda tidak perlu memahami kalkulus sekuen. Anda menulis assertion Rust, dan solver memberi tahu Anda apakah mereka berlaku. Itu bukan bukti formal dalam artian akademis. Itu adalah bukti mekanis dalam artian praktis, dan untuk sebagian besar perangkat lunak, praktis adalah persis apa yang Anda butuhkan.

Pertanyaan yang Sering Diajukan

Apa itu model checking dalam verifikasi perangkat lunak?

Model checking adalah teknik otomatis yang mengeksplorasi secara eksaustif semua keadaan yang mungkin dari sebuah sistem untuk memverifikasi apakah properti yang ditentukan berlaku. Untuk Rust, alat seperti Kani menggunakan bounded model checking untuk membuktikan assertion atas semua input yang mungkin dalam batas yang ditentukan, tanpa memerlukan konstruksi bukti manual.

Bagaimana Kani berbeda dari menulis unit test?

Unit test memeriksa satu input spesifik. Bukti Kani memeriksa setiap input dalam batas. Jika bukti Kani lulus, Anda tahu tidak ada counterexample dalam ruang keadaan terbatas. Buktinya lebih kuat, tetapi terbatas oleh batas yang Anda tetapkan.

Dapatkah Kani membuktikan seluruh aplikasi Rust saya benar?

Tidak. Kani bekerja paling baik pada fungsi kecil dan terbatas. Ruang keadaan tumbuh secara eksponensial dengan iterasi loop, kedalaman rekursi, dan ukuran data. Gunakan Kani untuk komponen safety-critical seperti parser dan handler protocol, bukan untuk logika tingkat aplikasi.

Apa yang terjadi ketika Kani menemukan loop tanpa batas tetap?

Kani memerlukan batas unwind untuk loop. Jika loop mungkin dieksekusi lebih banyak kali daripada yang diizinkan batas, Kani menyisipkan unwinding assertion yang gagal. Anda harus menaikkan batas atau merefactor kode agar memiliki jumlah iterasi yang diketahui secara statis. Ini adalah keterbatasan utama dari bounded model checking.