Barrier-Lyapunov-Agent: Training and Verifying Safe and Stable Neural Network Controllers

Certifying learned controllers requires coordinating certificate synthesis, formal verification, and controller refinement, a process that often involves substantial manual effort. We propose Barrier–Lyapunov Agent, a tool-augmented large language model framework that automates this process for systems with known dynamics or unknown dynamics. The framework follows three stages: objective understanding, Lyapunov-guided stabilization, and barrier-guided safety certification. Given a task specification and an initial controller, the agent generates structured tool arguments, constructs generalized Lyapunov and control barrier functions, and uses verification feedback to guide certificate updates and controller refinement. Upon successful verification, the framework returns the refined controller, corresponding certificates, and a report specifying the verified properties and their domains. Certification claims are determined by formal verification tools rather than by the language model. We evaluate the framework against two baselines using the same computational tools: a human-operated workflow and an agent without explicit workflow instructions. To assess the contribution of the tool suite, we compare the fully equipped Barrier–Lyapunov Agent with an otherwise identical AI agent without access to these tools. Our results show that controllers trained by the proposed agent achieve better control performance and larger formally verified regions of stability and safety than those produced by the baselines.