2 papers
cs.LO2026
A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
Natalia Klaus, Juan Conejero, Palina Tolmach
We describe a verification pipeline that takes production Rust cryptographic code and produces machine-checked correctness proofs in Lean 4. The pipeline combines three components:…
cs.PL2025
Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics
Jianhong Zhao, Everett Hildenbrandt, Juan Conejero +1
Verification proofs encode complete program behavior, yet we discard them after checking correctness. We present compiling by proving, a paradigm that transforms these proofs into…