3 papers
cs.SE2026
HarnessLLM: Rust Verification Harness Generation with Large Language Models
Minghua Wang, Yuwei Liu, Lin Huang
Rust's ownership model and type system offer strong memory safety guarantees, but unsafe code and runtime panics still present significant risks. Formal verification is essential t…
cs.SE2026
KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification
Minghua Wang, Yuxi Ling, Mingzhi Gao +2
Rust's ownership and type system provide strong memory safety guarantees, but unsafe code still presents memory safety risks. Formal verification is crucial for ensuring memory saf…
cs.SE2026
KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code
Yuwei Liu, Xinyi Wan, Yanhao Wang +3
Formal verification provides the highest assurance of software correctness and security, but its application to large-scale, evolving systems remains a major challenge. While large…