Evidence
Claims you can check
Every number and safety claim on this site, stated precisely: what was measured or proven, how it was measured, under which assumptions — and where the boundary of the claim sits.
How to read this page
Each card states one claim exactly as the site makes it, with its date or release version, the environment and methodology behind it, and — just as deliberately — what it does not cover. When a figure is re-measured, the card is updated with it: these are dated claims, not slogans.
Measured vs. proven
We keep two vocabularies apart. Proven means machine-checked in a proof assistant, over exact real arithmetic, about the mathematical model. Measured means benchmarked on hardware, with the sample counts and environment on record. Latency numbers are measured, never proven; safety theorems are proven, never inferred from test runs. The bridge between the real-number model and the floating-point implementation is checked numerically at runtime by an SMT solver portfolio — it is not itself a theorem.
CfC kernel inference
Measured December 2025 · GIDE benchmark corpus
A single closed-form continuous-time (CfC) cell — the reference inference kernel — completes one forward pass in 0.767 µs on average.
Methodology
Arithmetic mean over 10,000 sequential inference calls after 1,000 warmup iterations, cross-checked on independently attributed hardware. Every run — environment, figures, attribution — is published on the benchmarks page.
Not covered
This is the reference kernel, not a deployed controller — deployed controllers are substantially larger and complete in the tens of microseconds, still inside the real-time budget. And no latency figure is formally proven: timing is measured, never a theorem.
Faster than real time
Derived from the measured 0.767 µs · 100 Hz control budget
13,000× is a derived margin, not a separate measurement: a 100 Hz control loop budgets 10 ms per tick, and 10 ms ÷ 0.767 µs ≈ 13,000×.
Methodology
The numerator is the control-loop period GIDE targets (100 Hz); the denominator is the measured mean kernel latency above. The margin therefore inherits every scope caveat of the 0.767 µs figure.
Not covered
The multiple applies to the reference kernel. Deployed controllers are larger and slower — see the hardware runs — yet still clear the same 10 ms budget by roughly two orders of magnitude. No real-time bound is formally proven.
Theorems machine-checked
As of GIDE release v2026.07.1 · July 2026
219 theorems in the GIDE framework are machine-checked. 31 of those are complete — mechanized end-to-end in both Lean 4 and Isabelle/HOL with zero local axioms. The other 188 are machine-checked modulo explicitly declared local axioms: named real-analysis backbones, each documented and tracked for discharge.
Not covered
The proofs are over exact real arithmetic: they cover the mathematical model, not the compiled floating-point implementation — that bridge is checked numerically at runtime, and closing it formally is open, tracked work. Framework assumptions (Lipschitz continuity, compact sets, bounded disturbance, hardware isolation) are declared inputs, not theorems.
Formal safety guarantees
Complete, zero-axiom theorem cluster · Lean 4 + Isabelle/HOL
The safety core is a cluster of complete theorems — machine-checked end-to-end in both provers with zero local axioms — covering forward invariance of the safety set and Control Barrier Function filtering.
What is proved
Nagumo forward invariance: a barrier that starts non-negative and satisfies the inward-rate condition stays non-negative for all forward time. Existence of a safe control under the CBF condition, and that the minimally-invasive CBF-QP leaves an already-feasible nominal control unmodified. Robustness of the invariance argument under learning updates, effective safety margin under measured latency, and keep-out-set feasibility including preservation under zero-order hold.
Assumptions
Controllability is carried as a named hypothesis, not re-proven. Safety margins are constant or linear-rate — general nonlinear class-K rates are out of scope. Dynamics are deterministic with bounded disturbance; the keep-out results are static state bounds, not general obstacle avoidance.
Not covered
No microsecond or latency bound is proven anywhere in the proof corpus — any "proven microsecond safety" phrasing would be false, and we do not use it. Stochastic settings are out of scope. As above, the theorems govern the real-number model; the floating-point implementation is checked numerically at runtime.
Domains shipped
One verified core, specialized at compile time
Every domain listed here builds and runs end-to-end against the same verified core. Shipped means the domain exists as a working subsystem with its own harness — maturity varies and is stated per domain below, not rounded up.
Cart-pole control
The original demonstration domain: 3D cart-pole balancing with machine-checked CBF safety filtering.
Quadrotor flight
6-DOF rigid-body dynamics under a hybrid cascade controller, with the deployed configuration benchmarked end-to-end.
Financial markets
Live FX market data and paper trading against the Oanda API, driven by a 36-objective training curriculum.
Language models
Entropy, grounding, and safety regulation for language-model control behind a multi-tier governance pipeline.
Autonomous software
The youngest domain: an autonomous spec → build → verify loop, currently approaching its first fully autonomous cycle — we say so rather than round up.
What we deliberately do not publish
The cards above are designed to make our claims falsifiable without opening the engine. The following stay private: core source code, proof-generation automation, model weights, the controller architecture, optimization methods, customer data, and complete proof scripts.
For qualified partners
Under NDA we can provide an evaluation dossier, run a black-box benchmark on hardware you control, or arrange supervised inspection of sensitive artifacts in a controlled environment.