LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification.

arXiv:2610.30524v1 Announce Type: cross Abstract: Lyapunov functions and barrier certificates give state-space guarantees of stability and safety, but synthesizing and verifying them---especially for nonlinear, high-dimensional systems---remains an open challe