A blueprint for 'canonical' proof-carrying code promises order-of-magnitude cuts in the cost of routine software changes by removing accidental variation, but current evidence is preliminary and stops short of demonstrating preserved behavior, verification at scale, or real cost savings.
Frontier coding models may spend substantial capacity learning not only program behavior, but also accidental entropy in human repositories. Such repositories contain valuable signals: tests, incidents, migrations, edge cases, product judgment, and operational history. These signals are entangled with framework churn, naming drift, generated-source ambiguity, dependency rituals, CI dialects, weak proof routes, and human-oriented review customs. We propose agent-first canonical code, a proof-carrying substrate that rewrites routine product software into canonical behavior profiles, typed change algebra, proof lanes, constrained edit grammars, semantic patch cells, runtime negative memory, and proof-carrying change objects. The core hypothesis is that quotienting software by behavior equivalence under a declared oracle can collapse equivalent encodings into governed representatives with explicit evidence and proof obligations. The endpoint is amortized cost per verified correct change, including source, context, reasoning, tools, verification, security, provenance, review, failed loops, defects, and foundry cost under a common oracle. Reported reduction bands are hypotheses, not measured frontier results. The proposed limit is a No-Accident Horizon: removable accident decreases until residual novelty, evidence, governance, risk, and future optionality dominate. For supported routine-product distributions, this gives a defensible planning target near 100-fold all-in cost reduction, not a guarantee for all software. Preliminary QLoRA experiments on Qwen2.5-Coder-14B show that 64,088 canonical trajectories are learnable and suppress tested forbidden-language markers, but do not establish behavior preservation, scaling economics, or verified-change cost. The contribution is a falsifiable program centered on minimum functional description length and verified-change cost.
Summary
Main Finding
Frontier coding models pay large costs learning accidental human-code representation rather than durable software behavior. Porting routine product software into an agent-first canonical, proof-carrying substrate before training and before agent operation can (in principle) sharply reduce those costs across training, inference/reasoning, repair loops, verification, and review. The paper frames this as a falsifiable research program: the decisive metric is amortized all-in cost per verified correct change under a declared behavior oracle and paired raw vs canonical experiments.
Key Points
- Core thesis: train agents on the quotient of program space by a declared behavior oracle (P/∼O), not on the high-entropy human implementation orbit. A canonical representative plus evidence, renderer, and disposition ledger should replace many accidental degrees of freedom.
- Canonical substrate elements: canonical profiles, behavior cells, generated truth boundaries, typed change algebra, proof lanes, constrained edit grammars, reasoning digests, semantic patches, runtime negative memory, and proof-carrying change objects.
- Fourfold cost of raw repositories: models "pay" for accidental representation during (1) pretraining, (2) context gathering at inference, (3) reasoning/tool/retry loops, and (4) human review.
- Falsifiable experiment design: paired same-model comparisons on raw vs canonical repositories from the same lineage, with identical issues, hidden tests (behavior oracle), reviewer rubrics, and detailed measurement of files opened, tokens used, tool calls, failed repair lanes, verification runs, review burden, wall-clock time, and accepted-patch rate.
- Quantified payoff bands (Table I): conservative / central / aggressive ranges for different denominators. Representative central claims:
- Training tokens to fixed accepted-change target: 30×–150× reduction.
- Context/reasoning/tool/retry tokens per verified change: 10×–100× reduction.
- All-in cost per verified correct change: 10×–50× reduction.
- Dense-active serving speed (matched-quality canonical specialist vs large dense baseline): 8.3×–10×.
- Dense-active infra cost/token: 88%–90% lower (central).
- Important denominators and definitions emphasized: raw vs canonical tokens, Rentropy (entropy reduction), Rtrain (tokens-to-target), Rreason, Rretry, Rinvalid, Rcost (all-in verified-change cost), Raction (legal action-space reduction). The paper stresses that numbers must be tied to these denominators and validated empirically; they do not multiply arbitrarily.
- Preliminary evidence: QLoRA experiments on Qwen2.5-Coder-14B with 64,088 canonically translated trajectories show learnability and suppression of some forbidden-language markers — but these do not demonstrate behavior preservation, scaling, or verified-change economics.
- Risks and failure modes spelled out: canonicalization could (a) fail to reduce same-model cost, (b) require similar or more tokens to reach capability, (c) lose compatibility/behavior, (d) have foundry/verification overheads that consume gains, or (e) merely move entropy into metadata instead of eliminating it.
- Theoretical limit: No-Accident Horizon — canonicalization can remove removable accident only until residual novelty, evidence needs, governance, and risk remain; mature foundries plausibly approach an upper defensible limit of ~100× reduction in all-in verified-change cost for routine product work, not an unlimited guarantee.
Data & Methods
- Experimental design (front-door measurement ledger):
- Primary empirical tests:
- Same-model cost per accepted change on paired raw vs canonical repositories with same lineage and hidden oracle.
- Tokens-to-target accepted-change capability under paired scaling curves (same model architecture, raw vs canonical corpora).
- Dense-active infra cost/token and throughput comparisons at matched quality (canonical specialist vs dense baseline).
- Behavior-preservation checks: hidden tests, replay/fuzzing, migration checks, security checks, and human review to measure preservation tiers.
- Measurement ledger items to capture: files opened, context tokens, reasoning tokens, tool calls, failed repair lanes, hidden-test pass rates, verification reruns, reviewer time, and wall-clock time.
- Definitions (selected, operational):
- Behavior oracle O: declared tests/contract/invariants used to define preservation equivalence.
- Equivalence relation p1 ∼O p2 if O(p1) = O(p2). Canonical map κ: [p]O → (s, e, r, d) where s = canonical spec, e = evidence bundle, r = renderer, d = disposition ledger.
- Entropy and reduction metrics: Hhuman = H(representation | behavior, contracts, environment). Rtrain, Rentropy, Rreason, Rretry, Rinvalid, Rcost, Raction are reduction ratios comparing raw vs canonical denominators.
- Tools and prior art leveraged: program analysis and IR work (OpenAPI, protobufs, MLIR), semantic patches (Coccinelle), code query (CodeQL), e-graphs and rewriting, DreamCoder/library learning — combined into a canonicalization pipeline rather than mere deduplication.
- Preliminary training evidence: small-scale QLoRA fine-tuning showing canonicalized examples are learnable and can suppress certain markers. The paper is explicit that this is not sufficient evidence.
- Assumptions and falsification criteria: the paper lists nine explicit assumptions each with tests; the crucial gates are (1) same-model immediate cost improvement, (2) tokens-to-target benefits under paired scaling, and (3) lower all-in verified-change cost in production/amortized settings.
Implications for AI Economics
- Data quality as capital: If canonical substrates deliver the claimed Rentropy and Rtrain reductions, the effective "data per useful token" increases, lowering compute required to achieve a given software-writing capability. This could materially reduce marginal training compute demand for routine-product software capabilities.
- Shifts in returns and specialization:
- Foundry-model economics: canonicalization favors centralized, reusable foundries that build and amortize canonical cells, proof lanes, and verification infrastructure. High fixed costs and large reuse could drive winner-take-most dynamics in tooling and canonical datasets.
- Labor market effects: routine CRUD, CI, migration, and integration work could see large productivity gains and lower per-change costs, shifting human labor demand toward higher-novelty engineering, systems design, domain expertise, governance, and edge-case handling.
- Capital intensity vs compute demand:
- Per-change compute and inference costs may fall (lower token budgets, fewer retries), but capital investment in canonicalization tooling, verification, legal/compliance infrastructure, and proof-carrying runtime could increase. Net compute demand depends on adoption rates and the extent canonical tokens replace raw tokens across training corpora.
- Pricing and productization:
- If canonical substrates are proprietary or gated, they become valuable assets (data + proof infrastructure). Licensing models, subscription fees for canonical foundries, or vertically integrated AI providers bundling canonical training and inference could change competitive dynamics.
- Verification and provenance become billable features. Customers may value lower all-in verified-change cost and faster wall-clock change times, enabling premium pricing (or cost savings) for "proof-carrying" changes.
- Infrastructure and vendor dynamics:
- Dense-active inference costs per token may drop on canonical tasks, favoring smaller, specialist models and edge deployments for supported product classes. Conversely, broad models remain necessary for out-of-distribution and bespoke tasks.
- Hardware demand could bifurcate: less demand for brute-force long-token pretraining on raw corpora for routine tasks, but increased demand for verification tooling, formal methods compute, and serving/storage of canonical artifacts and proofs.
- Risk & regulatory economics:
- Canonical proof-carrying artifacts improve provable compliance, auditability, and security posture; this reduces economic risk for adopters and could influence insurers, regulators, and procurement decisions.
- Governance, legal risk, and provenance bookkeeping create overhead that must be priced into the all-in cost; if these overheads are large they can erode theoretical token-based gains.
- Empirical economics required:
- The paper’s insistence on denominators (cost per verified correct change) is an economic best practice — metrics must account for retries, verification, human review, downstream defects, and amortized engineering/foundry costs.
- Until paired raw-vs-canonical field trials are run and measured on the stated denominators, economic impact claims remain hypotheses. The distribution of gains across training, serving, verification, and amortization will determine market outcomes.
Practical takeaways for researchers and practitioners
- Prioritize paired experiments that measure all-in cost per verified change (tokens, wall time, tool calls, verification, review).
- Invest in canonicalization tooling that preserves evidence bundles, proof lanes, and migration/compatibility metadata, not only textual deduplication.
- Design verification and evidence standards (behavior oracles) upfront: the canonical quotient depends on the oracle.
- Evaluate where canonicalization is economically sensible: routine, repeatable product software likely has the largest near-term ROI; high-novelty code less so.
- Track risks: lost useful implementation diversity, under-specified oracles, and verification overheads that could negate gains.
Short list of critical validation checks (falsification criteria)
- Does a broad model presented with canonicalized repositories (same lineage) expend materially fewer tokens, tool calls, and reviewer time to produce an accepted, proof-carrying change?
- Under paired scaling curves, do canonical corpora reduce tokens-to-target capability for the same model architecture?
- In production trials, does the canonical approach lower all-in amortized cost per verified correct change after accounting for foundry and verification overhead? If these gates fail, the central thesis — that canonical proof-carrying substrates materially and reliably reduce the economic cost of agentic software change — is falsified or must be substantially narrowed.
Assessment
Claims (9)
| Claim | Direction | Outcome | Confidence & Evidence | Details |
|---|---|---|---|---|
| Frontier coding models may spend substantial capacity learning not only program behavior, but also accidental entropy in human repositories. Research Productivity | negative | model_capacity_usage (learning wasted/noisy patterns) |
Reading fidelity
high
Study strength
speculative
|
not reported
|
| Human code repositories contain valuable signals such as tests, incidents, migrations, edge cases, product judgment, and operational history. Developer Productivity | positive | value of repository signals for software understanding / maintenance |
Reading fidelity
high
Study strength
medium
|
not reported
|
| Those valuable signals are entangled with framework churn, naming drift, generated-source ambiguity, dependency rituals, CI dialects, weak proof routes, and human-oriented review customs. Organizational Efficiency | negative | degree of entanglement between signal and accidental repository noise |
Reading fidelity
high
Study strength
speculative
|
not reported
|
| We propose an agent-first canonical code, a proof-carrying substrate that rewrites routine product software into canonical behavior profiles, typed change algebra, proof lanes, constrained edit grammars, semantic patch cells, runtime negative memory, and proof-carrying change objects. Organizational Efficiency | positive | feasibility of a proof-carrying canonical-code substrate |
Reading fidelity
high
Study strength
speculative
|
not reported
|
| Quotienting software by behavior equivalence under a declared oracle can collapse equivalent encodings into governed representatives with explicit evidence and proof obligations (core hypothesis). Organizational Efficiency | positive | degree of encoding collapse / reduction of accidental representations |
Reading fidelity
high
Study strength
speculative
|
not reported
|
| For supported routine-product distributions, this approach gives a defensible planning target near 100-fold all-in cost reduction (amortized cost per verified correct change), though this is a hypothesis and not a guarantee for all software. Firm Productivity | positive | amortized all-in cost per verified correct change |
Reading fidelity
high
Study strength
speculative
|
near 100-fold all-in cost reduction
|
| Preliminary QLoRA experiments on Qwen2.5-Coder-14B show that 64,088 canonical trajectories are learnable and suppress tested forbidden-language markers. Ai Safety And Ethics | positive | number of learnable canonical trajectories and suppression of tested forbidden-language markers |
Reading fidelity
high
Study strength
medium
|
n=64088
64,088 canonical trajectories are learnable and suppress tested forbidden-language markers
|
| Those preliminary experiments do not establish behavior preservation, scaling economics, or verified-change cost. Research Productivity | null_result | establishment of behavior preservation / scaling economics / verified-change cost |
Reading fidelity
high
Study strength
high
|
not reported
|
| The contribution is a falsifiable program centered on minimum functional description length and verified-change cost. Research Productivity | positive | existence of a falsifiable research program around minimum functional description length and verified-change cost |
Reading fidelity
high
Study strength
speculative
|
not reported
|