collaborators

1 paper

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:…