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

📝 Paper Summary

Formal Verification Control Theory Neural Certificates

Fossil2.0 is a software tool that concurrently synthesizes neural control laws and formal certificates (such as Reach-While-Avoid) for dynamical systems using a counter-example guided inductive synthesis loop.

Core Problem

Verifying complex temporal properties (like reaching a goal while avoiding unsafe regions) for dynamical models is computationally difficult, and existing tools often lack support for rich specifications or concurrent controller synthesis.

Why it matters:

Safety-critical applications like robotics and autonomous vehicles require formal guarantees that they will avoid unsafe states while completing tasks.
Prior tools like SOStools or Fossil 1.0 were limited to simpler properties (stability/safety) or continuous-time models only, restricting their utility for complex real-world scenarios.

Concrete Example: A robot needs to reach a target zone while avoiding obstacles and then remain there (Reach-Avoid-Remain). Standard stability analysis only proves convergence to a point, not obstacle avoidance or finite-time reachability, requiring a composite certificate that existing tools could not automatically synthesize.

Key Novelty

Unified Neural Certificate and Controller Synthesis via SMT

Extends formal verification beyond simple stability/safety to complex specifications like 'Stable While Avoid' (SWA) and 'Reach-Avoid-Remain' (RAR) by synthesizing composite certificate functions.
Synthesizes neural control laws concurrently with certificates, using a cosine-similarity loss to guide the system toward the goal while the certificate proves compliance.
Integrates a new SMT solver (CVC5) within a CEGIS loop to provide sound, formal guarantees over continuous domains, unlike purely empirical testing.

Breakthrough Assessment

7/10

Significant expansion of formal verification capabilities to complex temporal logic specifications and discrete-time models, though the paper presents a tool update rather than a fundamental new theoretical paradigm.

⚙️ Technical Details

Problem Definition

Setting: Verification and control of dynamical models (ODEs or difference equations) against temporal specifications.

Inputs: Dynamical model f(x, u), Specification sets (Initial, Unsafe, Goal, Final), Domain definitions.

Outputs: Neural Network Certificate V(x) (proving the property) and optionally a Neural Control Law u(x).

Pipeline Flow

Learner (Neural Network Training)
Verifier (SMT Solver)
Refiner (Counter-Example Buffer)

System Modules

Learner

Trains neural network candidates for certificates and controllers based on finite sample sets.

Model or implementation: Feed-forward Neural Network (Template)

Verifier

Formally checks if the candidate functions satisfy the specification conditions over the entire dense domain.

Model or implementation: CVC5 (SMT Solver)

Novel Architectural Elements

Concurrent synthesis architecture: Optimizes control parameters for trajectory guidance while simultaneously optimizing certificate parameters for formal proof generation.
Modular certificate templates allowing composition of properties (e.g., combining reachability and avoidance) for complex specifications like RAR.

Modeling

Base Model: Feed-forward Neural Networks (used as function approximators for certificates)

Training Method: Counter-Example Guided Inductive Synthesis (CEGIS)

Objective Functions:

Purpose: Guide the control law to align vector fields with the direction towards the origin.

Formally: Cosine similarity loss penalizing trajectories that point away from the origin.

Key Hyperparameters:

statistical_methodology: Not explicitly reported in the paper

Comparison to Prior Work

vs. Fossil 1.0: Supports discrete-time models, control synthesis, and 5 additional specification types (ROA, SWA, RWA, RSWA, RAR).
vs. SOStools: Handles non-polynomial dynamics and non-convex sets via neural templates.
vs. Neural Lyapunov Control (NLC): Provides formal guarantees via SMT verification rather than just empirical loss minimization, and supports broader safety/reachability specs.

Limitations

Computational complexity of SMT verification scales poorly with high-dimensional state spaces.
The synthesis of control laws is based on soft-constraints (loss functions) and may require tuning to find valid controllers.

Reproducibility

The paper presents a software tool 'Fossil 2.0', but the specific GitHub URL is not included in the provided text snippets. It mentions a Python-based interface and command-line usage.

📊 Experiments & Results

Evaluation Setup

Formal verification of dynamical models (ODEs and difference equations) against safety and stability specifications.

Benchmarks:

Dynamical Model Benchmark Suite (Verification and Control Synthesis) [New]

Metrics:

Verification Result (Success/Fail)
Computational Time
Robustness
Statistical methodology: Not explicitly reported in the paper

Main Takeaways

Fossil 2.0 significantly expands the scope of verifiable properties from simple stability/safety to complex temporal specifications like Reach-Avoid-Remain (RAR).
The tool enables the synthesis of certificates for discrete-time models, addressing a gap in the previous Fossil 1.0 release.
Concurrent synthesis allows the tool to learn control laws that guide systems to satisfy specifications while simultaneously generating the proof of satisfaction.
The authors claim improvements in computational time and robustness compared to SOStools and NLC, though specific numeric results were not present in the provided text.

📚 Prerequisite Knowledge

Prerequisites

Control Theory (Lyapunov stability, Barrier functions)
Formal Methods (SMT solvers, CEGIS)
Neural Networks

Key Terms

Lyapunov function: A scalar function used to prove the stability of a dynamical system; if the function decreases along trajectories, the system converges to an equilibrium.

Barrier function: A function used to prove safety; it acts as a 'barrier' that trajectories cannot cross, ensuring the system never enters an unsafe set.

CEGIS: Counter-Example Guided Inductive Synthesis—an iterative loop where a learner proposes a solution and a verifier either proves it correct or provides a specific counter-example to retrain the learner.

SMT: Satisfiability Modulo Theories—a type of automated logical reasoning used here to formally prove whether a certificate function satisfies required conditions over a continuous domain.

ROA: Region of Attraction—the set of all initial states from which the system trajectories eventually converge to the equilibrium point.

RWA: Reach While Avoid—a property requiring trajectories to reach a goal set in finite time without entering an unsafe set.

SWA: Stable While Avoid—a property requiring trajectories to converge to an equilibrium while avoiding unsafe sets.

RAR: Reach-Avoid and Remain—a property requiring trajectories to reach a goal, avoid unsafe sets, and then stay within a final set indefinitely.