Algebraic design docs did not meet the +0.1 quality target in six tested conditions
Across six tested conditions, no algebra arm met the +0.1 quality target. That target was set before the build runs and applied to retrieval after its runs. No docs is the code-only control: it receives no supplementary documentation about the codebase. Judged quality was usually close to that control. Builder token and time effects changed with the task. These are small, descriptive comparisons on one application, not an estimate of the method’s effect on coding agents generally.
Results at a glance
The build rule required a +0.1 quality gain at every scored stage. Retrieval now uses the same quality target in a retrospective analysis. Each row below compares an arm with No docs in the same run. The quality rubric explains the score.
| Builder / runs | Arm | Quality Δ | Builder tokens Δ | Builder time Δ | Python CC Δ |
|---|---|---|---|---|---|
| gpt-6-sol · medium · 1 run | Prose docs | −0.010 | +5% | −1% | −0.33 |
| Algebraic docs | −0.070 | +32% | +2% | +0.96 | |
| gpt-6-luna · xhigh · 1 run | Prose docs | +0.060 | +30% | +31% | −0.17 |
| Algebraic docs | +0.070 | −7% | −1% | −0.65 | |
| gpt-6-astra · xhigh · 1 run | Prose docs | −0.008 | +12% | +6% | −0.02 |
| Algebraic docs | −0.007 | +75% | +35% | +0.15 | |
| gpt-6-sol · medium · 1 run | Prose docs | +0.013 | −5% | −16% | +0.96 |
| Algebraic docs | −0.003 | +37% | +11% | +0.79 | |
| gpt-6-sol · medium · 2 runs | Algebraic docs + z3 | +0.017 to +0.025 | −36% to −7% | −29% to +9% | −0.88 to −0.27 |
| gpt-6-sol · medium · 3 runs | Algebraic docs + z3 | −0.082 to +0.005 | +15% to +21% | −3% to −2% | −0.52 to +2.01 |
| gpt-6-sol · medium · 1 run | Prose docs | −0.028 | +26% | +0.2% | — |
| Algebraic docs + z3 | −0.042 | +22% | +3% | — | |
| gpt-6-luna · medium · 1 run | Prose docs | +0.020 | −22% | +9% | — |
| Algebraic docs + z3 | −0.080 | −8% | −4% | — | |
| gpt-6-sol · medium · 3 runs | Prose docs | +0.002 to +0.036 | +1% to +71% | −3% to +10% | 0.00 |
| Algebraic docs + z3 | −0.006 to +0.008 | +26% to +49% | +2% to +22% | 0.00 | |
Ranges show the smallest and largest paired run results for each builder and arm. Quality Δ is the difference in mean judge score over shared scored stages; tokens and time cover every stage the builder worked. Python CC Δ is the difference in recorded mean cyclomatic complexity of Python blocks at the final Python stage (the stage before Rust conversion where applicable), arm minus same-run control; — means no Python measurement.
How to read this: Positive quality Δ favors the named arm. Negative token or time Δ means the builder used less. The experiments used different tasks, models, and in the first condition a different judge; do not pool these rows into one effect size. Failed runs can still contain scored earlier stages. Each condition page shows which stage failed.
Cyclomatic complexity: For Rust-conversion conditions, Python CC comes from the final Python stage before conversion. The retrieval condition builds no code, and the large-codebase measurements include about 400,000 lines of vendored code. These values are descriptive and cannot support one aggregate complexity effect across conditions.
What was compared
Within a run, each arm got the same task and prompts in its own workspace. The control had no supplied design docs; other arms received prose or algebraic design material, sometimes with z3 proofs. The agent built one application in stages, or answered questions about its code in the retrieval condition. Each stage built on that arm’s own prior work.
Control
No docs
No design method and no starting design. Before coding, it writes its own method, then its designs.
Comparison
Prose docs
A design method in prose, and four starting charters in prose that define the application’s core concepts: checks, operations, the ontology and telemetry.
Hypothesis arm
Algebraic docs
A design method in algebra (capability contracts, Hoare triples, laws and proofs), and the same four charters in algebra, each with a written proof.
Hypothesis arm
Algebraic docs + z3
Algebraic docs, with each charter and proof also as a z3 file, and z3 installed. It must check its algebra with z3 before writing code, and every proof must pass when a stage ends.
Hypothesis: Describing a codebase algebraically instead of semantically reduces inference via proofs which reuse repeated reasoning.
The conditions change task length, prompt style, starting code, available design material, or builder model. They are separate scoped comparisons, not a sequence that isolates one factor between every row. Select a condition above for its stage results and run records.
What quality means
A separate judge read each arm’s code and rated seven qualities. The weighted score runs from 0 to 1. The rule for build conditions required an algebra arm to beat No docs by at least 0.1 at every scored stage of every counted run. Retrieval now uses the same +0.1 quality target, recalculated after the runs; it also requires token and time savings. Retrieval used a different rubric, so its quality scores should not be pooled with build scores.
| Quality | Weight | Basis for the judge’s rating |
|---|---|---|
| Ownership | 20 | Rules have one owner; functions do not mix unrelated jobs. |
| Boundaries | 15 | Components do not rely on another component’s private state. |
| Change locality | 20 | Three planned changes can be added without reworking existing parts. |
| Contracts | 15 | States, write decisions, and failures have clear definitions. |
| Simplicity | 10 | No redundant state or unused layers. |
| Readability | 10 | Names and concepts stay clear and consistent. |
| Testability | 10 | Checks and state changes can be tested in isolation. |
Each quality is rated 0–4 by defects the judge can point to; 4 means none found. Change locality instead counts how many of the three planned changes need rework. The weighted rating is divided by 4. For retrieval, the judge rated seven sections of each answer against the code, then divided the total by 28.
Variation and limits
Noise. In the 3 sets of runs that each repeat the same setup, the same arm’s score at the same stage moved by a median of 0.03 and at most 0.11, over 35 comparisons; 4 of them moved by as much as the rule’s threshold. The pooled standard deviation of one arm’s score is 0.030. With one to three runs per condition, small differences are hard to separate from run variation.
- Three conditions use different builder models across runs, so those runs are not repeats.
- The first condition used Claude Fable 5.1 as judge; the others used Claude Opus 5.5. Scores across that change are not directly comparable.
- All conditions build or read the same application. The findings do not establish results on other codebases.
- A run marked failed can retain scores from earlier stages. The table names its status and the number of shared scored stages.
Inspect the evidence - arm quality score delta from control
Generation · fresh codebase · 1 imperative stageQuality target: gain ≥ +0.10 at every scored stage
Generation · fresh codebase · 5 imperative stagesQuality target: gain ≥ +0.10 at every scored stage
Generation · fresh codebase · 5 imperative stages · z3-checked algebraQuality target: gain ≥ +0.10 at every scored stage
Generation · fresh codebase · 7 declarative stages · z3-checked algebraQuality target: gain ≥ +0.10 at every scored stage
Retrieval · 400k-line codebase · 5 questions · z3-checked algebraRetrospective retrieval target: correctness gain ≥ +0.10 · token and time savings also required
Generation · 400k-line codebase · 5 imperative stages · z3-checked algebraQuality target: gain ≥ +0.10 at every scored stage
The calculation is arm score - control (no documentation) at each scored stage, on one zero line. All conditions now use a +0.1 quality target. Retrieval’s target was chosen after its runs; its original rule allowed a 0.1 correctness loss. The condition pages hold stage checks, failure details, and run IDs. The Telos project explains the larger idea behind algebraic charters.
Data and methods
G001.json, exported from the harness tracking store by notebooks/export_findings.py using notebooks/findings/G001.yaml at harness commit 4486667, supplies the results on these pages. It identifies counted and excluded runs, their checks, and per-run application and grader commits and seeds.
The exported data supports inspection of these comparisons. The full run artifacts, harness, and dependent repositories are currently private, so readers cannot rerun the experiment from this page alone.