# Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models

arXiv: https://arxiv.org/abs/2311.09793 · HTML: https://mlsanity.com/paper/2311.09793/

## Key facts

- Cited by 15 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 28 references that are in the map.
- First posted on arXiv 16 Nov 2023.

## Builds on (most cited first, 12 of 12)

- [Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methods](https://mlsanity.com/paper/2202.11762/) (2022)
- [Neural Lyapunov Control](https://mlsanity.com/paper/2005.00611/) (2020)
- [Stability Verification in Stochastic Control Systems via Neural Network Supermartingales](https://mlsanity.com/paper/2112.09495/) (2021)
- [Learning Control Policies for Stochastic Systems with Reach-avoid Guarantees](https://mlsanity.com/paper/2210.05308/) (2022)
- [Safety Certification for Stochastic Systems via Neural Barrier Functions](https://mlsanity.com/paper/2206.01463/) (2022)
- [Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers](https://mlsanity.com/paper/2007.10865/) (2020)
- [A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis](https://mlsanity.com/paper/2309.06090/) (2023)
- [Counterexample Guided Synthesis of Switched Controllers for Reach-While-Stay Properties](https://mlsanity.com/paper/1505.01180/) (2015)
- [SOSTOOLS Version 4.00 Sum of Squares Optimization Toolbox for MATLAB](https://mlsanity.com/paper/1310.4716/) (2013)
- [Formal Synthesis of Lyapunov Neural Networks](https://mlsanity.com/paper/2003.08910/) (2020)
- [Formal controller synthesis for hybrid systems using genetic programming](https://mlsanity.com/paper/2003.14322/) (2020)
- [Formal Synthesis of Analytic Controllers for Sampled-Data Systems via Genetic Programming](https://mlsanity.com/paper/1812.02711/) (2018)

## Built on by (most cited first, 15 of 15)

- [Global Lyapunov functions: a long-standing open problem in mathematics, with symbolic transformers](https://mlsanity.com/paper/2410.08304/) (2024)
- [Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates](https://mlsanity.com/paper/2405.14058/) (2024)
- [Two-Stage Learning of Stabilizing Neural Controllers via Zubov Sampling and Iterative Domain Expansion](https://mlsanity.com/paper/2506.01356/) (2025)
- [Formally Verified Physics-Informed Neural Control Lyapunov Functions](https://mlsanity.com/paper/2409.20528/) (2024)
- [Safe Domains of Attraction for Discrete-Time Nonlinear Systems: Characterization and Verifiable Neural Network Estimation](https://mlsanity.com/paper/2506.13961/) (2025)
- [Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation](https://mlsanity.com/paper/2511.06341/) (2025)
- [LUCID: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems](https://mlsanity.com/paper/2512.11750/) (2025)
- [Analytical Lyapunov Function Discovery: An RL-based Generative Approach](https://mlsanity.com/paper/2502.02014/) (2025)
- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [Neural Proofs for Sound Verification and Control of Complex Systems](https://mlsanity.com/paper/2512.18389/) (2025)
- [Kernel-Based Learning of Safety Barriers](https://mlsanity.com/paper/2601.12002/) (2026)
- [Set-Based Training of Neural Barrier Certificates for Safety Verification of Dynamical Systems](https://mlsanity.com/paper/2605.02526/) (2026)
- [k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics](https://mlsanity.com/paper/2605.20108/) (2026)
- [Certificate-Guided Evaluation of Reinforcement Learning Generalization](https://mlsanity.com/paper/2606.00840/) (2026)
- [Neural Slack Variables for Shape Constraints](https://mlsanity.com/paper/2606.13803/) (2026)

## Abstract (arXiv)

This paper presents Fossil 2.0, a new major release of a software tool for the synthesis of certificates (e.g., Lyapunov and barrier functions) for dynamical systems modelled as ordinary differential and difference equations. Fossil 2.0 is much improved from its original release, including new interfaces, a significantly expanded certificate portfolio, controller synthesis and enhanced extensibility. We present these new features as part of this tool paper. Fossil implements a counterexample-guided inductive synthesis (CEGIS) loop ensuring the soundness of the method. Our tool uses neural networks as templates to generate candidate functions, which are then formally proven by an SMT solver acting as an assertion verifier. Improvements with respect to the first release include a wider range of certificates, synthesis of control laws, and support for discrete-time models.