A Design Theory for AI-Assisted Software Development Derived from Christopher Alexander’s Theory of Form

(authored by agents unless marked 🧑) Tag: chen2026design, paper

scope and result

The paper proposes Misfit-Governed Development (MGD) for unreliable LLM code generation. It makes requirements and local engineering tradition explicit, derives detectable misfits, and accepts a candidate only after deterministic gates find none. Its process has an autonomous inner loop and human outer loop, summarized as S = P = T = W: specification, program, tests, and world. The paper says, “The builder cannot change this machinery on its own authority.” (Abstract, p. 1). The model separates machine-checkable relations from the human judgment that the specification still fits the world.

technique 1: problem-frame specification and four-form pattern language

Use this before generation when a project has local architectural rules and externally meaningful requirements. Build problem-side files: frame.yaml for frame type and world facts, requirement files with descriptions/rationale/acceptance criteria, a machine specification, a domain specification, and acceptance.yaml in Given–When–Then form (Section 3.2, p. 12). On the solution side, encode every pattern in four coupled forms: doctrine (when/why), template (positive code skeleton), prohibition (what must not appear or be absent), and gate (deterministic checker plus good/bad fixtures and real invocations). The paper states, “A pattern that exists only as prose is treated as not existing, because prose guidance alone does not reliably constrain the builder.” (Section 3.4, p. 20).

Keep a single-source-of-authority registry for duplicated rules; restatements remain full text for the builder, while machine links and self-consistency checks detect divergence. Treat gates as law at design time and harness at run time. Guidance may inform an LLM but cannot pass or halt a build. Inference: for Verus, templates can include Rust/Verus idioms, prohibitions can forbid unverifiable escape hatches, and gates can run verus, compilation, and source checks. The paper’s architecture is Java/Spring/React, so the exact files and gates do not carry over; the authority separation does.

technique 2: deterministic gate stack

Run a stack of blocking detectors after generation and after every repair. The reference stack has 28 blocking gates: specification-quality linting; dual-profile tests; 18 per-use-case structural gates; seven aggregate closeout gates; and a deterministic review applying 188 machine-checkable rules (Section 3.5, p. 21). Structural gates check scenario and contract coverage, field agreement through value objects/entities/events/mappers/persistence/DTOs, and controller boundary behavior. Closeout checks catch chain errors invisible to local inspection, such as dropped fields or unwired reactions. Every gate is an ordinary program, parser, matcher, or test run; no LLM is in its verdict path. A skipped gate is not a pass.

Verus form (Inference): make each gate a reproducible script that records source revision, Verus version/options, dependencies, output, and pass/fail; use requires/ensures and proof functions only inside the verified Rust target, while external structural checks remain trusted tooling. Preserve gate evidence as an attestation input, but do not claim that gate execution proves specification completeness. The paper explicitly keeps semantic faithfulness beyond deterministic predicates in an advisory three-LLM review, whose findings go to human adjudication.

technique 3: bounded repair loop and legislative boundary

Verus form (Inference): let the repair agent edit executable Rust and Verus proof bodies, then rerun the verifier and tests; protect specifications, gate scripts, and attestation metadata with repository permissions and require human approval for changes. A Verus proof pass remains evidence for the encoded contract only.

Classify failures into test, structural, and pattern layers. Batch all findings within one layer, send each with offending code, violated rule, and authoritative pattern pointer, then regenerate. Re-run all prior gates after each repair because fixes can break earlier properties. Halt and escalate if the violation count fails to decrease for three consecutive rounds. Freeze the specification, framework version, tradition, and verification machinery during the loop. The paper states, “A round needs only to reduce the violation count and to avoid breaking what already passed.” (Section 3.6, p. 23). The builder may modify generated artifacts but cannot write gate verdicts, rules, templates, or workflow state; amendments use a human-gated legislative circuit (Section 3.7, p. 24).

evidence, limits, and VL threat

The case study rebuilt a Scrum backend from 64 problem-frame specifications across four aggregates. Each aggregate’s latest rebuild passed all blocking gates and generated tests under both profiles. The snapshot reports approximately 1,300 tests, 28 blocking gates, 188 deterministic rules, 53 architecture decision records, and more than 3,500 tests for gate modules (Table 3, p. 31). Recorded telemetry covered 5,807 runs from 1 March–16 August 2026, with 216,148 violation reports at 1,748 distinct rule-and-file sites across 235 historical rules. PIT test strength was 95–100% killed/covered mutants across four aggregates, but the paper cautions that PIT “say[s] nothing about whether the tests are faithful to the acceptance scenarios.” (Section 5, p. 32).

What is proved/measured is operation of one methodology and its gates on one system. Trusted are human-authored specifications, rule correctness, detector coverage, framework/runtime behavior, and the world fit S=W. The authors do not claim universal architecture binding or that an LLM has learned the tradition. Inference: the threat to agent-written verified Rust is requirement omission and gate blind spots: Verus can prove the encoded contract while a field, integration behavior, or environmental assumption remains absent. MGD’s explicit human outer loop and frozen, reproducible verifier evidence are useful for VL, but implementing the full 28-gate analogue would be costly. VL should reuse the four-form pattern and repair/escalation ideas rather than redo generic LLM prompting or ordinary test gates.

techniques for the catalog

• problem-frame specification: encode world facts, requirements, machine/domain responsibilities, and Given–When–Then acceptance scenarios before generation
• four-form patterns: pair doctrine, code template, prohibition, and deterministic gate as one enforceable pattern
• deterministic gate stack: block on specification, tests, structural traceability, architecture, and machine-review rules with no LLM verdict path
• bounded repair loop: batch findings, re-run previous gates, freeze context, and escalate after three stagnant rounds
• human legislative boundary: let the builder repair generated artifacts while humans approve changes to rules, templates, and gates Checked 2026-10-14 against the paper by a Codex agent: audit record chen2026design; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: 2026-10-15