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.
An unpublished technical report with Florian Zeba at Alpha Omega Labs, dated June 2026. It has not been peer reviewed and is not posted to a preprint server, so treat everything below as a working draft rather than a settled result. I describe it here because the formal framing is useful independently of whether the numbers survive review.
The problem
Coding agents fail in two unrelated ways, and the industry mostly patches one of them.
The first is safety. Under adversarial input — a malicious instruction in a repository file, in tool output, or in memory — an agent can be induced to exfiltrate secrets or run destructive commands. The standard response is a guardrail: inspect each action, block the bad ones.
The second is quieter. Over a long task, agents silently abandon requirements. They complete the early, legible parts of a specification and let the tail go, and because nothing errors, nothing signals the job is unfinished.
A guardrail cannot help with the second failure, and that is the report’s central observation. Filtering actions is a negative capability: it can remove an unsafe action but cannot supply direction. A filter cannot plan a long-horizon task. Safety and completion need different machinery.
The idea
Cortex is a meta-level control layer wrapped around an existing agent harness. It does not replace the base model; it supervises it, along two axes.
Governance handles safety as a projection: deterministic pre-execution checks and capability policies restrict the agent to an admissible subset of actions. The unsafe action class is removed structurally rather than declined case by case.
Orchestration handles completion. A task is analysed into a set of requirements plus a contract, and then the agent runs what the report calls the Synapse loop: execute against the requirements still open, validate the result with an oracle, and repair whatever the verdict flagged.
The formal content is in how that loop is modelled. 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, which 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 must stabilise: the loop reaches a least fixed point, a state where another pass adds nothing, in at most as many productive passes as there are requirements. The loop reports success exactly when the required set is contained in that fixed point. And the fixed point does not depend on the order in which requirements were satisfied, so two runs that schedule work differently agree on the outcome.
The comparison this sets up is sharp. A single-pass harness applies the operator once. The governed loop computes its closure. Halting when a pass adds nothing is not a heuristic stopping rule; it is fixed-point detection.
A further proposition connects 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.
Why it matters, and what it does not prove
The experiments compare paired arms — same base model, prompt and 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, about a 43% relative reduction, and from 3.4% to 1.7% on a base model that was already much safer, in both cases at comparable over-refusal. Blocking attacks by refusing everything would be trivial; holding over-refusal flat is what makes the number mean anything.
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, which the report argues is the correct outcome: the layer supplies control, not additional model capability, and a task covered by one validated increment gives the loop nothing to add. Gains concentrate on the long-horizon families, where single-pass arms complete early milestones and decay across the tail.
The limits are stated in the report and worth repeating. The theorem guarantees the loop converges; it says nothing about the value of the fixed point. How much of a specification is reachable depends on the base model’s productivity per pass, so absolute completeness stays model-dependent. The trajectory-similarity metric’s absolute scale depends on the embedding used. A single full-repository run trades variance for cost. And, again, none of this has been refereed.
Where it applies
The most portable piece is the experimental protocol rather than the layer.
Most published comparisons between coding agents confound the control loop with the model, so a “better agent” may just be a better model. Cortex’s protocol 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. A baseline that silently inherited that configuration would flatter itself and void the comparison. Anyone benchmarking harnesses can copy the discipline, whatever they make of the theory above.