AI Labs AI Labs
Localized frontier research

AGIOS

An agent OS substrate and a specialist-model factory. AGIOS turns open-weight base models into verified vertical specialists — a teacher demonstrates, a machine oracle certifies, and the student trains only on traces that survived certification. Frontier-shaped work, run locally.

Concept design

Inside the AGIOS Observatory

The operator console this substrate is built toward — three scenes from it: the substrate's components as a live constellation, a program's trip through the kernel verifier, and the flagship benchmark laid out as a bar, not just a number.

The load-bearing idea

The oracle's verdict is the training label

Which means the entire system's correctness reduces to one thing: the oracle must be benchmarked, un-gameable and sound before its verdicts are ever trusted to train weights. Get that right and a small model becomes a specialist. Get it wrong and you train a model to be confidently wrong.

Teacher
Demonstrate
A frontier model demonstrates solutions and proposes candidate verification logic. Independent certification — not the teacher — decides whether that oracle may admit traces.
Oracle
Certify traces
The trust root. Only verified trajectories survive as training data.
Student
Distill + train
LoRA on the verified traces — base model swappable.
Result
A specialist
A vertical-specific adapter, scoped to the family its oracle can verify.
↻ repeat per vertical while preregistered evidence shows improvement — stop on plateau, regression or falsification
The quality gate

Only traces accepted by a currently certified, mutation-tested oracle are eligible for training. Certification reduces label-corruption risk; it cannot eliminate it. An unsound or compromised oracle can still poison training — so provenance, quarantine, held-out evaluation and human audit remain required.

The flagship result

Kernel-verified eBPF authoring

The first vertical has an agent autonomously write eBPF programs judged by the real Linux kernel verifier — compiled, verified, loaded, attached, triggered, and their BPF maps read back — inside a hardened, disposable VM with no host mounts. A bad program panics the guest, never the host.

Scoring is behavioural. "Correct" means the program attaches, fires on the right events and its map holds the right counts — not merely that it loaded.

SetupMean accuracyRange (n=3)Cost / run
AGIOS verify loop ON100.0%100 / 100 / 100~$0.165
Same model, raw (loop OFF)81.5%77.8 – 88.9~$0.064
Measured delta

+18.5 percentage points, with 0% variance against 11pp variance, at ~2.6× cost. Same model, same temperature, same tasks, same independent ground-truth judge. The delta is the substrate's measured contribution — not the model's.

Caveats, logged with the experiment

Single model. Nine tasks. The baseline is "no infrastructure at all". We publish these limits alongside the number, because a result whose caveats you have to go looking for isn't a result.

Is the problem real?

EXP-026 — a preregistered kill condition

The argument for certified oracles is only worth making if production verifiers are actually unsound. So we fixed the condition in advance: if the defect rate on real verifiers is near zero, the thesis is wrong and the work stops. All 24 rule-based verifiers were extracted from a public instruction-following suite, and good, bad and adversarial cases were written fair to each verifier's own documentation.

8 / 24
unsound — wrongly accept bad output (6 on the conservative count)
13 / 24
defective — unsound or broken (11 conservative)
33%
unsound rate; the thesis survived its own kill condition
Every
oracle certified internally had a real hole — including frontier-designed ones
Why the bar is so high

At training time, the worker becomes an adversary

The optimizer drives toward whatever passes — that's reward hacking, and Goodhart's law: when a measure becomes a target, it ceases to be a good measure. An oracle that is fine for an occasional inference check is not good enough to train on. The training-grade bar is far higher than the inference-grade bar.

Oracle errorWhat it meansConsequence
False positiveOracle says ✓ on actually-bad outputCatastrophic — poisons the weights
False negativeOracle says ✗ on actually-good outputSafe — merely wastes a good example
Design law, every vertical

Sound ≫ complete. Tune against false positives on the versioned certification set, at the cost of false negatives. Wasting a good example is recoverable. Poisoning the weights is not.

Can a small model do it?

Split the work by role — the answer isn't one number

Not "can a small model match a frontier model in general?" — no. But "can a fine-tuned specialist do our bounded work as well as the teacher does it?" For the verifiable majority, yes. A narrow specialist beats a general giant on its own turf.

The roleWhat it takesFine-tuned specialist?
Worker
execute in a vertical, satisfy the oracle
Pattern-following inside a defined harness against a machine judgeAlready doing it
Architect — known patterns
reuse an existing oracle
Map a goal onto a proven vertical shapeMostly yes
Architect — novel oracle
design a sound judge for an unseen domain
Open-ended reasoning; highest stakes; distills worstHard ceiling — keep the teacher
Read the status labels

What is built, what is gated, what is unproven

Every claim in the AGIOS research record carries one of three labels. We think that is the minimum standard for publishing work like this.

Implemented

Harvesting, certification, the frozen benchmark and the hash-chained ledger. Durable resumable runtime, separate control and worker planes, governed memory, protocol gateways, and policy-enforced model spend.

Operational gate

Sound-oracle coverage, still being expanded vertical by vertical. Also: the PostgreSQL profile is tested but experimental, and fails HA readiness until replicated crash/failover certification is checked in.

Unproven hypothesis

That repeated verified-trace distillation yields durable, cross-family local improvement. Labelled as unproven throughout, with a preregistered condition that would disconfirm it. The current eligible-trace count is 0 — and we report that number, not the flattering denominator.

The headwinds, stated plainly

Reasoning ceiling — fine-tuning teaches patterns it has seen; it won't grant frontier generalization to genuinely new structures. Distribution-bound — excellent on-distribution, brittle off it. Oracle design is irreducibly hard — the step that most needs frontier reasoning is the one least suited to a small model, and the most dangerous to get wrong.