Verification

Import this file for TorchLean’s verification infrastructure: JSON utilities, certificate formats, ODE/PINN-style checkers, proof-backed certificate soundness, and the proof-backed TorchLean-to-IR forward compiler bridge.

Their expression parsers share the fuel-bounded byte cursor and decimal scanners from NN.Verification.Util.TextCursor; each verifier keeps only its grammar and AST-specific logic.

The compiler bridge is imported through NN.Verification.TorchLean.Proved, which contains both the compiler and its correctness theorems.

Runnable CLIs stay out of this umbrella. If you want a command-line tool, import the registry explicitly (for example NN.Verification.CLI).

The underlying CROWN/LiRPA soundness development enters here too. Executable examples can parse JSON artifacts and recompute bounds inside Lean; theorem-level credit comes from those imported soundness modules, where locally valid certificates are connected to Lean graph semantics.