TorchLean API

NN.Entrypoint.Verification

Verification entrypoint #

This is the public umbrella import for TorchLean’s verification infrastructure: JSON utilities, certificate formats, ODE/PINN-style checkers, proof-backed certificate soundness, and the verified TorchLean-to-IR forward compiler bridge.

We keep one verification entrypoint on purpose. The verified compiler bridge is imported here through the naming-friendly NN.Verification.TorchLean.Verified API, so users do not have to choose between separate “proved” and “verified” umbrellas.

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

Proof-backed certificate workflows enter here too. Executable examples can parse JSON artifacts and recompute bounds inside Lean; theorem-level credit comes from the imported CROWN/LiRPA soundness development, where locally valid certificates are connected to Lean graph semantics.