I used multiple AI agents (and Lean) to formally validate a Rust algorithm. Along the way the AI tried to hide missing proofs. I describe the process and surprises.