6 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…
Mengapa model checking mengalahkan berhari-hari runtime produksi untuk menemukan bug konkurensi, dan cara menerapkannya pada kode Anda sendiri.
Menunggu race conditions muncul di produksi bukanlah pengujian. Itu adalah harapan yang menyamar sebagai ketekunan. Anda bisa menjalankan aplikasi selama…
Bounded model checker seperti Kani dan relational model finder seperti Alloy memungkinkan Anda memverifikasi properti dengan assertion dan constraint biasa. Anda mengorbankan pembuktian liveness untuk kurva pembelajaran yang diukur dalam jam, bukan minggu.
Anda tidak perlu mempelajari logika temporal linear untuk menggunakan model checker. Alat seperti Kani, CBMC, dan Alloy memungkinkan Anda memverifikasi…
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…
Bug terdistribusi mahal untuk diperbaiki setelah deployment. Model checking memungkinkan Anda menemukannya sebelum menulis satu baris kode implementasi pun. Berikut cara melakukannya dengan TLA+.
Anda tidak bisa melakukan unit test pada protocol terdistribusi. Unit test menjalankan satu proses di satu mesin dalam satu urutan. Protocol Anda menjalankan…