Nama : Al Ghifari Enerza Sentanu Program Studi : Sistem Informasi Judul : Pemanfaatan Prusti untuk Memverifikasi Bahasa Pemrograman Rust Pembimbing : Amril Syalim, S.Kom., M.Eng., Ph.D. Rust adalah bahasa pemrograman sistem yang dikenal akan fitur keamanannya seperti ownership dan borrowing yang menjamin keamanan pada memori. Namun tidak semua keamanan dijamin oleh compiler Rust. Salah satunya karena adanya keyword unsafe yang tidak dicek oleh compiler. Prusti adalah alat verifikasi formal untuk bahasa Rust. Penelitian ini bertujuan untuk mengevaluasi seberapa akurat Prusti dalam memverifikasi program Rust. Eksperimen dilakukan dengan melakukan uji coba pada topik seperti conditional, operasi matematika, recursion, loop, indexing, borrowing dan fungsi unsafe. Program tersebut diverifikasi menggunakan Prusti lalu keluaran dari verifikasi dibandingkan dengan hasil yang diharapkan. Hasil penelitian menunjukkan Prusti akurat dalam memverifikasi program sederhana, namun memiliki keterbatasan untuk menangani fitur Rust yang belum didukung oleh Prusti seperti keyword unsafe. Untuk penelitian lanjutan, disarankan memperluas cakupan eksperimen ke fitur Prusti lainnya. Meskipun demikian, penelitian ini telah menunjukkan potensi Prusti dalam meningkatkan jaminan keamanan program Rust. Kata kunci: Rust, Prusti, verifikasi formal