9 posts
AutoVerus menggunakan jaringan agen LLM untuk menghasilkan proof kebenaran Verus untuk kode Rust, mengotomatisasi lebih dari 90% proof obligation melalui loop generate-repair-discharge yang didorong oleh feedback SMT solver.
Bagian tersulit dari verifikasi formal tidak pernah ada pada verifier-nya. Ada pada penulisan proof. Beri seorang engineer Rust senior Verus, verifier berbasis…
Model bahasa besar menulis kode Rust yang menakjubkan baiknya, tetapi ketika Anda meminta pembuktian formal, mereka menghasilkan invarian yang tidak ada dan menciptakan sintaks yang tidak diterima oleh verifikator apa pun. Berikut ini yang benar-benar mereka lakukan dengan benar, di mana mereka gagal, dan bagaimana menggunakannya meskipun begitu.
LLM dapat menulis Rust yang dikompilasi dan bahkan lulus . Apa yang tidak dapat mereka lakukan secara andal adalah menulis pembuktian formal bahwa kode…
Alat model checking seperti Kani memungkinkan Anda memverifikasi properti Rust dengan assertion alih-alih bukti formal. Masalahnya adalah apa yang terjadi ketika loop Anda tidak memiliki batas kecil.
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…
Standard library Rust memberikan otoritas filesystem ambient kepada setiap dependensi. cap-std menggantinya dengan API berbasis capability yang memaksa kode untuk membuktikan bahwa ia berhak mengakses suatu path sebelum membukanya.
Crate apa pun di pohon dependency Anda bisa membuka , menulis ke direktori Anda, atau menghitung setiap berkas di proyek Anda. Standard library Rust tidak…
Exception yang dilempar menyembunyikan jalur kegagalan dari sistem tipe Anda. Berikut mengapa pengembalian error secara eksplisit membuat kode Anda lebih jujur, dan cara mengadopsinya tanpa membuat Anda benci hidup.
Tanda tangan fungsi Anda mengatakan bahwa fungsi tersebut mengembalikan . Tidak. Fungsi tersebut mengembalikan atau meledak. Sistem tipe sama sekali tidak…
Struct wrapper satu-field menangkap bug pencampuran unit dan kebingungan tipe tanpa menambahkan satu byte pun overhead.
Lewatkan user ID ke fungsi yang mengharapkan order ID, dan Rust tidak akan protes. Keduanya adalah . Compiler melihat tipe yang identik, jadi ia tidak bisa…
cargo-mutants menemukan tes yang hanya berpura-pura memverifikasi kode Anda. Berikut cara kerja mutation testing di Rust, apa yang ditangkapnya, dan apakah biaya waktu kompilasi sepadan.
Anda memiliki 100% line coverage. Setiap branch tercapai. Setiap function dipanggil. Lalu seseorang mengubah menjadi di logika pricing Anda, menjalankan tes,…
Pengujian berbasis contoh hanya mencakup input yang Anda pikirkan. Property-based testing menghasilkan data acak, memeriksa invariant, dan menyusutkan kegagalan menjadi contoh kontra minimal.
Anda menulis fungsi . Anda mengujinya dengan dan . Lolos. Anda release. Seorang pengguna memberikan slice dengan satu elemen. Fungsi Anda membuangnya begitu…
Rust secara otomatis menghapus debug assertion, tetapi design-by-contract yang sesungguhnya membutuhkan lebih dari debug_assert!. Berikut cara membangun runtime contract tanpa biaya yang lenyap dari binary release Anda.
Rust dapat menegakkan runtime contract saat development dan menghapusnya sepenuhnya dari release build. Catatannya, bahasa ini tidak memperlakukan contract…