Vehicle is a dependently typed domain-specific language for specifying, training, and verifying safety properties of neural-network controllers. A specification is written as a logic formula over the network, and a class of logics called differentiable logics gives such formulas a real-valued semantic interpretation. This interpretation is used as a loss function during training to drive the network towards satisfying the formula.

In this work we extend the Vehicle specification language with the discrete-time, bounded temporal operators $\square_{[a,b]}$, $\Diamond_{[a,b]}$, and $\mathcal{U}_{[a,b]}$, together with a Time type, a @dynamics annotation for transition functions, and a rollout primitive that returns the full trajectory of a controller over time. The extension is conservative over the prior language and reuses Vehicle’s existing support for first-order quantifiers and differentiable logics, yielding a Signal First-Order temporal logic for cyber-physical controller synthesis; we know of no other surface language that exposes SFO in its specification syntax with a synthesis-time compilation. The temporal operators are defined generically over the underlying differentiable logic, and a soundness theorem (Reuse) certifies the construction for any host logic satisfying minimal regularity conditions, so adding a new differentiable logic requires no per-logic code or proof. At runtime, each temporal operator is evaluated in parallel over the trajectory by adapting the PyTorch differentiable-STL library STLCG++.

We synthesise adaptive cruise control networks from a single specification (with no behaviour-cloning data) and verify them against that specification by abstract-interpretation reachability; both spec-trained controllers outperform the published ARCH-COMP 2025 BC reference on every centre-evaluated property.

Keywords: Differentiable logics, Signal temporal logic, Signal first-order logic, Closed-loop control, Adaptive cruise control, CROWN reachability, Vehicle.