open-source applications

A benchmark for coding agents that tests whether they can formally verify properties of real-world Rust web apps in Lean 4. It includes upstream code, i5h ports, extracted Lean models, proof attempts, and task-by-task results.