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

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

Link from the fetch record. The paper text gives no DOI, arXiv identifier, or publisher page for this paper; it cites arXiv:2605.13357 as reference [2], a different paper by Zhong and Zhu.

scope and result

The paper proposes Misfit-Governed Development (MGD) for unreliable LLM code generation. It makes requirements and local engineering tradition explicit, enumerates mechanized misfits, and accepts a candidate when the harness detects none of those misfits. Its autonomous inner loop and human outer loop form the S = P = T = W assurance model: specification, program, tests, and world. These equals signs denote agreement relations, not literal equality. The paper says, “The builder cannot change this machinery on its own authority.” (Abstract, p. 1). Machines check structural specification/program agreement, structural scenario/test agreement, and test execution; humans judge whether the specification fits the world. Passing these checks does not establish absolute correctness (Appendix A, pp. 44–46).

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

The problem representation has five kinds of artifact per use case: frame.yaml for frame type, world facts, and frame concerns; requirement files with descriptions, rationale, and acceptance criteria; a machine specification; a frame-specific domain specification; and acceptance.yaml with Given–When–Then scenarios traced to requirements (Section 3.2, pp. 12–13). Specifications grow per use case rather than being completed up front. On the solution side, every pattern used for generation must have doctrine (when and why), a template (positive code skeleton), prohibitions (what must not appear or be absent), and a deterministic prerequisite check with good/bad fixtures and real invocations (Section 3.4, p. 20). The paper states, “The four forms divide the labor rather than duplicate it.” (Section 3.4, p. 20).

A single-source-of-authority registry identifies the original of each duplicated rule. Restatements remain full text for the builder; machine-readable links and consistency checks detect divergence (Section 3.4, p. 21). The governing rule belongs to the law; its executable checker belongs to the harness. Guidance cannot render a verdict or halt progress (Section 3, p. 10). Not every prerequisite check belongs to a pattern: specification-side checks enforce what the system must do, while patterns encode how the local tradition builds (Section 3.4, pp. 20–21).

Inference: for Verus, templates could express Rust/Verus idioms, prohibitions could restrict unverified escape hatches, and prerequisite checks could run Verus, compilation, and source checks. This would be a new binding; the paper evaluates Java/Spring Boot with a React/TypeScript frontend, and portability remains untested (Sections 5 and 8).

technique 2: deterministic prerequisite checks

The reference stack has 28 blocking prerequisite checks: one specification-quality check; one dual-profile test check; 18 per-use-case structural checks; seven aggregate-wide closeout checks; and one deterministic review applying 188 machine-checkable rules (Section 3.5, p. 21). Tests run under both in-memory and full outbox/PostgreSQL infrastructure profiles. Structural checks cover scenarios and contracts, field agreement through representations, and controller behavior. Closeout checks cover specification boundaries, deliverable manifests, encapsulation, and cross-frame consistency. Cross-aggregate checks are distributed across these groups. Every blocking verdict comes from an ordinary program, parser, pattern matcher, or test run, without an LLM in its verdict path (Section 3.5, pp. 21–22). A skipped check does not count as passed (Section 5, p. 30).

Two advisory prerequisite checks and an optional multi-model semantic review sit outside the blocking count. The review uses three vendor-distinct LLMs and an arbiter LLM; it remained advisory and its effect was not evaluated (Section 3.5, pp. 21–22). Appendix A.1 requires evidence that every mechanized predicate was evaluated, but the implementation uniformly tracks execution only at whole-check granularity. A narrowed or empty scan set can still produce a false pass inside a checker (Section 8, p. 42).

Inference: a Verus implementation could record the source revision, verifier version/options, dependencies, output, and result for each reproducible prerequisite check. Proofs establish the encoded contracts under the verifier’s assumptions; external structural checks remain trusted tooling. Such evidence does not establish specification completeness.

technique 3: bounded repair loop and legislative boundary

The repair loop has separate test, structural, and pattern layers. Each round batches violations within one layer. Findings include offending code, the violated rule, and a pointer into the tradition; the builder is instructed to reread the authoritative pattern, but that instruction is guidance. Every repair reruns prior prerequisite checks. The loop halts and escalates if the violation count fails to decrease for three consecutive rounds. Specifications and framework versions are pinned during the repair window; tradition and verification machinery change only through a separate process with human approval (Section 3.6, pp. 22–23). 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 cannot write verdicts or workflow state. Tradition files are protected differently: the builder can physically edit them, but those edits have no authority until a human accepts them; consistency checks flag divergent copies (Section 3.7, pp. 23–24). If a checker rejects conforming code, repair the checker. If the governing rule is wrong, revise it through human approval rather than changing code to satisfy a broken rule (Section 3, p. 11; Section 3.7, p. 24). Each escaped defect must extend or correct the mechanized enumeration, or receive an explicit ruling that identifies the alternative means covering it (Section 4.4, p. 28).

Inference: a Verus repair agent could edit implementation and proof bodies while human approval controls changes to specifications, prerequisite-check scripts, and evidence metadata. A proof pass would remain evidence for the encoded contract only.

techniques for the catalog

• problem-frame specification: encode world facts, requirements, machine/domain responsibilities, and Given–When–Then scenarios per use case
• four-form patterns: couple doctrine, template, prohibition, and a deterministic prerequisite check
• deterministic verification stack: check specifications, tests, structural traceability, architecture, and local rules without LLM verdicts
• bounded repair loop: batch findings within a layer, rerun previous checks, freeze context, and escalate after three rounds without a decrease
• human legislative boundary: let the builder repair generated artifacts while humans approve changes to governing rules and machinery

Last edited: 2026-10-19