verisolv: A Unified Artifact Bridging a Numerical ODE/PDE Solver and a Machine-Checked Convergence Proof

Verisolv is a single reproducible artifact pairing a SciPy-like numerical ODE/PDE solver with a machine-checked convergence proof. Python solver: 5 ODE methods plus 2 PDE solvers, with a SciPy-compatible API.Rust kernel (via PyO3): reproduces the Python RK4 trajectory bit-for-bit.Lean 4 proof: explicit Euler's global error is O(h), verified with zero sorry; #print axioms confirms only Lean's three standard axioms. Builds and validates end-to-end with four commands: pip install, pytest, cargo test, lake build. Co-authored by Anubhav Prasai and Himangsu Adhikari (AIYGO).