Skip to content

5 min

  • Category: Essay
  • research-paper
  • ai-agents
  • formal-methods
  • ai-safety

Cortex: a fixed-point theory of governed coding agents

Treating an agent's validate-repair loop as a monotone operator on a lattice of requirements, so that 'the task is done' becomes a least fixed point you can prove it reaches.

Written for this site.

A coding agent that tries to exfiltrate your credentials will get caught. A coding agent that quietly does eighty percent of what you asked will not.

Both are failures. Only one of them has an industry.

Two failures, one of which nobody guards

The first failure is adversarial. A malicious instruction hidden in a repository file, in tool output, or in the agent’s own memory induces it to leak a secret or run something destructive. The standard answer is a guardrail: inspect each proposed action, block the bad ones.

The second failure is quiet. Over a long task, agents abandon requirements. They finish the early, legible parts of a specification and let the tail go. Nothing errors. Nothing signals that the job is unfinished. You get a confident summary of work that is partly imaginary.

A guardrail cannot touch that, and this is the observation the whole report turns on. Filtering is a negative capability: it can remove an unsafe action, but it cannot supply direction. No filter, however good, will plan a long-horizon task or notice that requirement fourteen was never attempted. Safety and completion are not two settings on one dial. They need different machinery.

The construction

Cortex is a meta-level control layer around an existing agent harness. It does not replace the base model. It supervises it, along two axes that mirror the two failures.

Governance is a projection. Deterministic pre-execution checks and capability policies restrict the agent to an admissible subset of actions, so the unsafe class is removed structurally rather than declined case by case.

Orchestration is a closure. A task is analysed into a set of requirements plus a contract, and the agent then runs what the report calls the Synapse loop: execute against the requirements still open, validate the result with an oracle, repair whatever the verdict flagged, repeat.

The interesting part is what happens when you model that loop properly.

Track the state as the set of requirements satisfied so far, ordered by inclusion. Each pass applies an operator that adds exactly the requirements the validation oracle newly certifies. Because the ledger is append-only, the operator never removes anything. That makes it monotone — more input, more output — and inflationary — the state only ever grows.

Those two properties are enough for a theorem. The successive states form a non-decreasing chain bounded by the total number of requirements, so it has to stabilise. The loop reaches a least fixed point: a state where another pass adds nothing, in no more productive passes than there are requirements. Success is exactly the condition that the required set is contained in that fixed point. And because the operator is monotone, the fixed point does not depend on the order the requirements were satisfied in — two runs that schedule work differently agree on the outcome.

That reframes something that usually gets treated as a heuristic. A single-pass harness applies the operator once. A governed loop computes its closure. Stopping when a pass adds nothing is not a stopping rule bolted on for safety; it is fixed-point detection, and it is the definition of done.

A further proposition ties this to the observation that harness performance scales with effective feedback rather than raw compute. Feedback accumulated over a run equals the size of the fixed point — so when a task needs more than one validated increment, extra samples cannot substitute for extra governed iterations. You cannot parallelise your way out of a dependency chain.

What the experiments show

Paired arms: same base model, same prompt, same tools, with and without the layer, across five task families.

On safety the effect is large. Adversarial attack-success falls from 42.4% to 24.1% on one frontier base model — around a 43% relative reduction — and from 3.4% to 1.7% on a model that was already much safer. In both cases over-refusal stays comparable, which is the number that makes the result mean anything: blocking every attack by refusing everything is trivial, and holding over-refusal flat is what rules that out.

On capability the result is deliberately unexciting where it should be. On well-specified single-file tasks the governed and raw arms are at parity. The report argues this is the correct outcome rather than a disappointment: the layer supplies control, not model capability, and a task covered by a single validated increment gives the loop nothing to add. The gains concentrate in the long-horizon families — exactly where single-pass arms complete the early milestones and decay across the tail.

What it does not show

The theorem guarantees the loop converges. It says nothing about the value of what it converges to. How much of a specification is reachable depends on the base model’s productivity per pass, so absolute completeness remains model-dependent — the fixed point is a stopping guarantee, not a quality one.

Beyond that: the trajectory-similarity metric’s absolute scale depends on the embedding used, and a single full-repository run trades variance for cost.

The part worth stealing

If you take one thing from the report, take the protocol rather than the layer.

Most published comparisons between coding agents confound the control loop with the model, so a “better agent” may be nothing more than a better model. The protocol here isolates the loop. Each raw baseline runs in a fresh workspace outside the project tree, so directory-walking configuration discovery cannot reach the layer’s files, and the subprocess environment is stripped of the layer’s variables, so no hook, policy, skill or parent-session state leaks in.

That discipline matters more than it sounds. A baseline that silently inherited the layer’s configuration would flatter itself and void the comparison — and it is an easy mistake to make, because the inheritance is invisible and the numbers still look plausible. Anyone benchmarking harnesses can copy the setup, whatever they make of the theory above.


Joint work with Florian Zeba at Alpha Omega Labs, June 2026. The full report — definitions, proofs and the complete experimental tables — is here.

← All writing