Leveraging Large Language Models for Automated Proof Synthesis in Rust

Jianan Yao, Ziqiao Zhou, Weiteng Chen +1

Formal verification can provably guarantee the correctness of critical system software, but the high proof burden has long hindered its wide adoption. Recently, Large Language Mode…