Cortex governs coding agents to meet requirements through fixed-point theory
Cortex: A Fixed-Point Theory of Governed Coding Agents - Technical Report
Artificial IntelligenceMachine Learning
Summary
When computer programs are made by combining large language models with code editors and testers, it’s hard to ensure they meet all requirements. The authors study Cortex, a system that checks and fixes code before it runs by continually validating and updating it until everything fits together. They use math to prove this process reaches a stable point without endlessly looping. The study also measures how long it might take on average, given some ideal conditions. However, the proofs depend on some assumptions that may not hold in real-world settings like with faulty checks or limited time.
What this means in practice
- •For software development teams: Use formal validation steps to ensure iterative automated code editing converges to meeting project requirements under sound conditions.
- •For automated testing engineers: Estimate expected time to complete validation loops for test-driven repairs in coding agents under assumptions of positive progress.
A theory result. No direct application yet.
Authors
Marius-Constantin Dinu, Florian Zeba
Abstract
A coding agent combines a large language model (LLM) with a harness that plans, edits, and executes code. We study Cortex, a supervisory layer for pre-execution governance, requirement tracking, and iterative validation and repair. We formalize requirement closure on a finite lattice. For a fixed requirement set and a sound, monotone validation rule with persistent evidence, exhaustive iteration reaches the least fixed point with no more strict increases than there are requirements. Fair consequence scheduling reaches the same closure. A separate stochastic model bounds expected completion time under a uniform positive-progress assumption. These results depend on their stated assumptions; artifact repair, fallible validation, and finite execution budgets do not satisfy them automatically. We define Gauntlet's trajectory-similarity and build-gated scores, attack-success estimators, Wilson intervals, and case-cluster bootstrap summaries. Effective-feedback accounting counts newly certified requirements, rather than estimating their information value or utility. The five evaluation families support raw-versus-governed comparisons. We report retained benchmark observations, including rescoring of existing artifacts; constructed outcomes are excluded. Unequal observation sets and incomplete provenance prevent causal claims about governance or measured long-horizon scaling.