FormalCert-AI
FORMALCERT-AI
We study how learned systems can come with meaningful guarantees—from certificate synthesis and statistical certification to monitoring during deployment.
RESEARCH PROJECT · 2026 · WORKING PAPER
Anytime-Valid Runtime Monitoring of Learned Barrier Certificates
Auditing learned barrier certificates from observed trajectories, with anytime-valid false-alarm control under the conditional barrier-drift assumption.
RESEARCH PROJECT · 2026
LLM Synthesis of Certificates with SMT/Lean Verification
Lyapunov functions, barrier certificates, and feedback policies for stability, region of attraction, forward invariance, and safety.
Includes DynaCertBench: 105 problems spanning literature-derived, extended, and newly constructed systems.
NEW PROJECT · 2026 · PREPRINT
Statistical Certification of Neural Barrier Functions for invariance and Reach-Avoidance in Learning-Enabled Systems
Joint policy–barrier learning followed by independent PAC certification. Explore how a certified region’s size relates to its multi-step guarantee.
SELECTED WORK
Research on formal guarantees for intelligent and dynamical systems.
2025 · ARXIV PREPRINT
A comparison of barrier-like conditions for infinite-horizon reach-avoid verification in stochastic discrete-time systems, examining their guarantees, conservativeness, and computational tractability.
The LLM2Cert repository contains the implementation, benchmark, recorded model outputs, and experiment reproduction instructions.
The statistical certification project currently hosts the manuscript, with implementation updates to follow.