A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
Summary
A detailed experience report on integrating Rust-to-Lean extraction, cryptographic libraries, and AI provers to verify production Rust code. It documents pipeline architecture, a running example, AI-automation results, and engineering gaps, with open repositories for reproducibility.