# E024: Existing-codebase changes: z3 algebra missed the quality margin and used more tokens Condition: Generation · 400k-line codebase · 5 imperative stages · z3-checked algebra · Result: not supported · 2026-09-24 Here the design docs start already written for the existing application. Across three repeat runs, neither Prose docs nor Algebraic docs + z3 lifted the score by the threshold in any stage. Algebraic docs + z3 used more tokens than No docs in every run. ## Results at a glance | Run | Arm | Average score | Stages compared | Tokens | Time | Python CC | |---|---|---:|---:|---:|---:|---:| | E024 run 1 | No docs | 0.310 | 5 of 5 | **10.01M** | **0:50:31** | **3.27** | | | Prose docs | **0.312 (+0.002)** | | 17.16M (+71%) | 0:55:44 (+10%) | 3.27 | | | **Algebraic docs + z3** | 0.304 (−0.006) | | 14.93M (+49%) | 0:59:38 (+18%) | 3.27 | | Run | Arm | Average score | Stages compared | Tokens | Time | Python CC | |---|---|---:|---:|---:|---:|---:| | E024 run 2 | No docs | 0.310 | 5 of 5 | **12.05M** | 0:50:09 | 3.27 | | | Prose docs | **0.346 (+0.036)** | | 12.19M (+1%) | **0:48:45 (−3%)** | 3.27 | | | **Algebraic docs + z3** | 0.318 (+0.008) | | 16.61M (+38%) | 1:01:11 (+22%) | **3.27** | | Run | Arm | Average score | Stages compared | Tokens | Time | Python CC | |---|---|---:|---:|---:|---:|---:| | E024 run 3 | No docs | 0.294 | 5 of 5 | **12.21M** | **0:53:28** | 3.27 | | | Prose docs | **0.308 (+0.014)** | | 14.07M (+15%) | 0:57:44 (+8%) | 3.27 | | | **Algebraic docs + z3** | 0.292 (−0.002) | | 15.34M (+26%) | 0:54:31 (+2%) | **3.27** | Scores average the stages every arm of the run scored: the stages compared. Tokens and time are each run's builder totals over every stage it worked. Brackets compare with No docs. Highlighted values mark the highest quality score and lowest recorded tokens, time, and Python CC within each run; ties share the highlight. This does not mean the success rule passed. Python CC means the recorded mean cyclomatic complexity of the Python code's functions, classes, and methods at the final stage. It includes vendored code where present. ## What changed in this condition The agent extends an existing application inside about 400,000 lines of vendored code, over five stages of imperative prompts. - **No docs** (control): No design method and no starting design. Before coding, it writes its own method, then its designs. - **Prose docs**: The prose method, and the existing application's finished design in prose in place of the starting charters. - **Algebraic docs + z3** (hypothesis arm): The algebraic method with z3 installed, and the existing application's finished design in algebra, with its z3 files, in place of the starting charters. Every proof must pass when a stage ends. **Runs:** 3 (E024 run 1, E024 run 2, E024 run 3), repeats of one setup. **Builder model:** gpt-6-sol · medium **Agent harness:** `codex-cli`. **Judge:** `claude-opus-5-5-high`. ## Stage evidence **Not supported.** Each part of the rule must hold in every run. Stages: 1. `duplicate-name-check` 2. `entry-supersession` 3. `revise-information` 4. `agent-token-telemetry` 5. `ontology-audit` **✗ Algebraic docs + z3 must score at least 0.1 above No docs in every graded stage, in every run: not met** | Run | Arm | Met | 1 | 2 | 3 | 4 | 5 | |---|---|---:|---:|---:|---:|---:|---:| | E024 run 1 | **Algebraic docs + z3** | 0 of 5 | −0.02 | +0.02 | +0.03 | 0.00 | −0.06 | | E024 run 2 | **Algebraic docs + z3** | 0 of 5 | −0.01 | +0.01 | +0.06 | −0.03 | +0.01 | | E024 run 3 | **Algebraic docs + z3** | 0 of 5 | 0.00 | −0.07 | +0.04 | 0.00 | +0.02 | Each cell is the arm's score minus the other arm's at that stage. ✓ marks a stage that meets that part of the rule; Met counts them, of the stages with a value. **Noise.** Between runs that 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 15 comparisons; 2 moved by 0.10 or more, the rule's threshold. ## Details ### The prediction, set before the runs The test card names the arms as follows: `control` is No docs, `semantic` is Prose docs, `algebraic_solver` is Algebraic docs + z3; `total_tokens` is tokens and `elapsed_s` is time. > **Prediction.** The algebraic_solver arm's quality score exceeds the control's by at least 0.1 in each stage; tokens and time are recorded as secondary measures. > > **Falsifier.** The algebraic_solver arm's quality score is no higher than the control's. A positive difference below 0.1 is inconclusive. **Measured:** Each arm's judged `score` at each stage. Quality Δ is the arm's score minus No docs. A stage meets the quality target at +0.1 or above. Every counted check must pass in every run. ### z3 | Run | Arm | Last stage | Proof goals | Proved | Disproved | Undecided | Stages the agent ran z3 | |---|---|---:|---:|---:|---:|---:|---:| | E024 run 1 | **Algebraic docs + z3** | 5 | 222 | 222 | 0 | 0 | 3 of 5 | | E024 run 2 | **Algebraic docs + z3** | 5 | 201 | 201 | 0 | 0 | 4 of 5 | | E024 run 3 | **Algebraic docs + z3** | 5 | 187 | 187 | 0 | 0 | 3 of 5 | After each stage, the system runs z3 on the proof goals in the design's z3 files and counts those it proves, disproves or leaves undecided. The counts are from the last stage that has them; — means none were recorded. The last column counts stages in which the agent itself ran z3. ### Runs #### E024 run 1 — gpt-6-sol · medium **Run ID:** `run-20260924T013909Z-79df517b` **Started:** 2026-09-24 **Harness status:** completed Every arm finished every stage. #### E024 run 2 — gpt-6-sol · medium **Run ID:** `run-20260924T013934Z-a085b261` **Started:** 2026-09-24 **Harness status:** completed Every arm finished every stage. #### E024 run 3 — gpt-6-sol · medium **Run ID:** `run-20260924T014000Z-e4983936` **Started:** 2026-09-24 **Harness status:** completed Every arm finished every stage. ### Source data [View condition `E024` in G001.json](https://mikereese.dev/data/experiments/G001.json). The run IDs above identify the counted runs. See [Data and methods](https://mikereese.dev/experiments/g001/#data-and-methods) for the export method and limits.