Research / Autonomous systems
Verification and Assurance for Autonomous Systems
Autonomous systems are accepted on evidence: evaluation logs, test results and proofs about models. OMEGA checks whether that evidence says what it appears to say, and states what each check does not establish.
Research and engineering work. OMEGA has not certified any autonomous system. Nothing here is a regulatory approval, an accredited audit or a safety assessment of a deployed system.
Completed public work this draws on
- Robot-policy evaluation recordsMerged, released in inspect-robots 0.59.0inspect-robots pull request 425
- Scorer order changed a reported countReproduced and reported; fix by another contributor, mergedInspect AI case
- A green proof above an unconnected outputMerged, not yet in a tagged releasecommon_cells case
- A solver’s wrong satMerged, released in cvc5 1.4.2cvc5 case
- A spending cap proved for a protocol modelProved for the model, not for any implementationEscrow case
Autonomous-system evaluation
Making robot evaluations traceable
inspect-robots is an open-source evaluation framework for physical AI: models run on robot arms and humanoids, on real or simulated benchmarks. Runs graded by different models and rubrics could leave identical specifications in their logs. Each run now records its grader and settings, a change the maintainer had invited.
Boundary: A traceability change to evaluation tooling. It does not evaluate any robot, model or policy, and no physical robot was tested.
Formal verification
A proof covers what it states and nothing else. In the first case below, the defect sat beside a proof that passed.
A green proof and an unconnected output
All four properties proved, yet one declared output, syndrome_o, was never connected. A cover check exposed it; the one-line fix and the first formal proof of the module were merged.
Boundary: One undriven output in one module of one library. The fix is merged on main and is not yet in a tagged release.
A solver’s wrong sat
A cache keyed without polarity let cvc5 return a wrong sat on a separation-logic problem. The fix is released in cvc5 1.4.2. Another user found the failing input; the root cause was traced and the fix submitted in pull request 12937.
Boundary: One theory and one class of formula. The rest of cvc5 was not audited, and the failing input was found by another user.
A spending cap was proved to hold in every reachable state of a protocol model.
Proved in Lean 4 for any finite set of replicas and any non-negative amounts, including global crash and recovery. Four negative-control theorems show the bound breaks if a guard is removed.
Boundary: A proof about this model and this invariant, not about any implementation. Model-to-code correspondence is argued, not proved.
AI reliability
The same failing run reported 6 of 6 or 4 of 6 completed samples, depending only on scorer order.
Reproduced with a mock model and reported upstream (issue 4602). Another contributor wrote the fix, which was merged.
Boundary: One framework behaviour, one failing run, a mock model. Says nothing about any model score. The fix was written by another contributor.
An agent’s write limit
An AI agent’s tool server passed 66 of 66 tests and its own replay check said VERIFIED, while it wrote 100,000 bytes where it was allowed 4,096.
Boundary: Related public work, not client work. One system, one configuration.
Told to use deterministic algorithms, PyTorch produced 7 different outputs in 50 runs of the same sparse CUDA calculation.
Reproduced across three PyTorch versions.
Boundary: One GPU model (RTX 5090), the CUDA CSR matrix-vector path and one input. Reported upstream and not fixed; nothing is claimed about PyTorch’s deterministic mode in general.
Evidence and reproducibility
Every case page states the question, what was tested, what survived, what is still open, who did what, and how to reproduce or inspect the result. Status labels describe the kind of evidence, not its quality.
AI agents in the system do much of the implementation and checking. Where a command was not re-run for a page, the page says so.
Status labelsFixes and reports in other people’s softwareHow it works
Technical research collaborations
OMEGA is open to research collaborations with groups and engineering teams working on autonomous systems. Questions of this kind fit. They are examples of proposed investigations, not past work:
- Does an evaluation record contain enough to reproduce a reported robot-policy score?
- Does a property proved about a controller or protocol model still hold for the code that runs?
- Does a runtime monitor still fire when an input it depends on is missing or late?
- Which of two evaluation set-ups gives the more reliable answer before an expensive test campaign?
OMEGA is currently led by one person. Where a question needs domain expertise OMEGA does not have, the first reply says so.