PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Chien-Tsun Chen, Yu Chin Cheng

arXiv:2610.01372v1cs.SE

TL;DR

Because plausible LLM-generated code can conceal missed requirements, the paper derives a human-governed verification harness from Alexander’s theory of form. In its reported case, about 27% of the corpus contained the material requiring the most author judgment, while checks of whether tests captured scenario meaning remained structural.

  • Problem

    LLM-generated code cannot be assumed to meet requirements, and the verification stack needed to establish fit remains an open design question.

    Source: §1 · p. 2

  • Method

    The paper derives Misfit-Governed Development, combining explicit problem and tradition representations, deterministic misfit gates, a fix loop, and human governance.

    Source: §1 · p. 2, §2.4 · p. 6, §3 · p. 11

  • Results

    About 27% of the corpus, roughly 11,000 lines, contained the material requiring the most author judgment.

    Source: §5 · p. 32

  • Takeaways & Limitations

    The assurance approach leaves human judgment responsible for whether the specification fits the world rather than treating gate results as that verdict.

    Source: §1 · p. 2, §8 · p. 41

    Machines check tests structurally, but do not check whether a test verifies what its acceptance scenario actually meant.

    Source: §8 · p. 41

Abstract

from arXiv · show

Code generated by large language models (LLMs) cannot be assumed to meet specified requirements. Reviews, testing, and static analysis still apply, but which of them a sufficient harness needs, and in what role, is open. We propose a design theory derived from Christopher Alexander's theory of form, and a methodology for applying it. In Alexander's account, fit between a form and its context can be perceived only negatively, through the absence of identified misfits. We make the organization's tradition explicit and derive the misfits from it and from the problem's classification. The theory models the LLM as a non-native vernacular builder, trained on many codebases but native to none, whose output tends to drift toward mainstream conventions rather than the local tradition. We engineer four pieces of machinery: explicit representations of the problem (Jackson's problem frames) and of the tradition (a four-form pattern language); deterministic misfit detectors; a fix loop; and a human-gated legislative circuit governing the representations and detectors. We call the resulting methodology, a practice of harness engineering, Misfit-Governed Development (MGD). Its dual-loop process separates an autonomous inner loop, where the LLM iterates against the gates, from a human outer loop, where specifications are judged against the world. Together they form the S = P = T = W assurance model (specification, program, tests, world), whose equals signs name relations, not identity. We report evidence from building and rebuilding a Scrum system of four event-sourced aggregates from 64 problem-frame specifications, verified by about 1,300 generated tests and 28 blocking gates, one applying 188 rules. This addresses the generativity dimension of Alexander's 1996 OOPSLA challenge. The moral dimension, whether the specification still fits the world, requires human judgment and belongs to the outer loop.

1. Introduction

The paper asks how to verify that LLM-generated software fits its requirements and local context when plausible code can conceal misunderstandings. It derives a harness methodology from Alexander’s theory of form, separating machine-checkable misfit correction from human judgment about fit to the world.

1. Introduction

  • Plausible generated code can silently miss requirements, so apparent fluency and conventional review do not establish correctness.The paper frames the open design question as what a sufficient verification stack must contain and what theory can establish its sufficiency for a fit claim.Source: §1 · p. 2
  • Alexander’s theory treats fit as the absence of identified misfits, making the completeness of the enumerated misfit list central to verification.Functional correctness is only one misfit class; architectural, contractual, and local-tradition demands also matter.Source: §1 · pp. 2–3
  • The paper proposes Misfit-Governed Development, deriving a design theory that models the LLM as a non-native builder prone to mainstream defaults.Its machinery includes a four-form pattern language, explicit problem representation, deterministic gates, a fix loop, and human governance.Source: §1 · p. 3
  • The dual-loop assurance model assigns candidate iteration to machine gates and reserves judgment about whether specifications fit the world for humans.The equals signs in S = P = T = W name relations, not identity.Source: §1 · pp. 3–4
  • The methodology offers a graded answer to Alexander’s challenge: it operationalizes generativity while leaving experiential coherence and the moral question to human judgment.The paper presents its contributions as one chain, from the builder model through the pattern language and harness to the two-loop process.Source: §1 · p. 4

2. Background and the Derivation

The derivation turns Alexander’s theory of fit into engineering obligations for an LLM builder, while Jackson’s problem frames provide reusable structure for representing recurring problem concerns. It connects those obligations to a governed enumeration of misfits and corresponding mechanisms.

2.1 Fit, misfit, and the negative definition of good design

  • Fit is operationalized as the absence of every enumerated misfit, so the scope and completeness of that enumeration bound the machine’s verdict.Repairs rerun the enumeration, while misfits outside it remain for the outer loop’s judgment.Source: §2.1 · p. 4

2.2 The unselfconscious process and its enabling conditions

  • Vernacular building achieves fit through tradition, manifested failures, collocated perception and repair, and culturally determined interpretations of misfit.When these conditions fail, the Oregon Experiment provides a precedent for institutionalized diagnosis against a pattern language.Source: §2.2 · pp. 4–5

2.3 The arc to The Timeless Way and the OOPSLA challenge

  • Alexander’s explicit pattern language is scaffolding toward mastery, while his OOPSLA challenge asks whether software patterns preserve generativity, coherence, and moral purpose.The proposed endpoint of “forgetting” is when a builder responds directly to the forces without consulting the language.Source: §2.3 · p. 5

2.4 Problem frames

  • Jackson’s problem frames classify recurring problem types and concerns, providing a reusable starting structure for enumerating misfits beyond which projects add domain-specific ones.This amortizes part of the context analysis across problems of the same class.Source: §2.4 · p. 6

2.5 From propositions to obligations: the derivation, stated explicitly

  • The derivation maps Alexander’s propositions to obligations under the non-native-LLM premise, then maps those obligations to engineering mechanisms.The ten rows are not exhaustive: a new row is warranted only when an escape exposes an obligation not covered by existing rows; the derivation claims unity, not exclusivity, since some obligations have other justifications.Source: §2.5 · p. 6, Table 1 · p. 7

3. The Methodology

Misfit-Governed Development (MGD) makes system requirements and local tradition explicit, then governs generated code through deterministic misfit checks and a bounded repair loop. Human judgment retains authority over changes to the tradition and verification machinery.

3. The Methodology

  • MGD admits candidates only when enumerated misfits are absent, and requires verification of the law and enforcement machinery as well as generated code.The law states what to produce and how; the harness renders verdicts and halts progress. The law and harness must be checked for integrity and fidelity to their sources.Source: §3 · pp. 9–10
  • False positives are repaired in the gate or law, never by changing generated artifacts, and only humans may approve amendments to the law.Detection cost sets feedback cadence: machine-priced checks support a continuous inner loop, while human-priced checks require a budgeted outer loop.Source: §3 · p. 11

3.1 The dual-loop model

  • The inner loop retries candidates against deterministic machine checks, while the outer loop uses observed behavior and lived consequences to revise representations and judge fit with the world.Persistent failures escalate to human diagnosis; machines verify S = P = T, while humans judge S = W and govern the law and harness.Source: §3.1 · pp. 11–12, Figure 2 · p. 12

3.2 The problem representation: problem-frame specifications

  • Use cases are classified into seven frame types and specified per use case; the authors add reactive invocation and connection frames to Jackson’s five types.Event Storming informs classification, and specifications grow piecemeal; connection frames lie outside the application tree and the paper’s empirical counts.Source: §3.2 · pp. 12–13

3.3 The solution-side language: a pattern network

  • The solution-side pattern network fixes the architecture before prompts, encodes local conventions, and supplies ordered, frame-specific generation traversals.Its Clean Architecture layers and boundaries support locality, while the traversal determines generation order rather than runtime call flow.Source: §3.3 · pp. 14, 19, 20

3.4 The four-form pattern language

  • Every pattern must couple doctrine, template, prohibition, and gate before the builder may generate from it.The rule and executable checker are authored together so the verdict stays coupled to the governing rule.Source: §3 · pp. 10–11, §3.4 · p. 20
  • The four-form language separates a pattern’s doctrine, code template, prohibitions, and deterministic gate from specification-enforcing gates on the problem side.Patterns must be machine-manifested; prose alone is insufficient. Each rule has a designated original, and consistency checks detect divergent restatements before generation; humans approve amendments.Source: §3.4 · pp. 20–21

3.5 The gate stack: manufactured manifestation

  • The gate stack includes 28 blocking gates, including 18 per-use-case structural gates and deterministic review applying 188 machine-checkable rules.Structural checks trace specified scenarios and fields across tests and code layers, while every gate returns the same verdict for the same artifact and pinned environment. Optional multi-model review is advisory, non-deterministic, and not reported as evaluated evidence.Source: §3.5 · pp. 21–22

3.6 The fix loop: mechanized vernacular repair

  • The three-layer fix loop batches test, structural, and pattern violations, re-runs prior gates, and escalates when progress stalls for three rounds.Repairs are anchored to the violated tradition by directing the builder to reread authoritative patterns. The judgment context stays fixed during the loop, and an uninterpretable specification also triggers escalation to a human.Source: §3.6 · pp. 22–23

3.7 What the builder may not touch

  • The builder may repair generated artifacts but cannot change gate verdicts or give tradition edits legislative standing without human approval.Tradition changes enter through a separate human-gated circuit, including defect post-mortems, saved improvement proposals, and audits; when a gate wrongly rejects conforming code, the gate is fixed instead.Source: §3.7 · pp. 23–24

4. Theoretical Analysis

The theory treats the generator as locally non-native and measures fit against explicit representations of the problem and tradition. Its machinery pairs automated artifact repair with human judgment over the representations and their fit to the world.

4.1 The non-native vernacular builder

  • The non-native vernacular builder is globally fluent but defaults toward mainstream idioms, so gates—not prompt guidance—decide whether outputs meet local doctrine.Because learned defaults are not shown to be replaced by in-context instructions, anti-mainstream rules remain active and must still be tested on bad fixtures and real artifacts.Source: §4.1 · pp. 24–25

4.2 Primary and proxy context

  • Primary contexts supply demand authority, while specifications and other proxies represent those demands and can silently diverge, requiring reconciliation.Primary demands may be empirical or created by authoritative rulings; proxies of a ruling can be checked against one another but not conclusively against the ruling itself.Source: §4.2 · pp. 25–26
  • S = P = T = W names machine-checked relations among specification, program, and tests within a human-judged relation between specification and world.The equals signs are mnemonic, not literal identity; validation of whether the specification fits the world remains a human judgment.Source: §4.2 · p. 27

4.3 Detection cost sets the affordable feedback cadence

  • Automated inner-loop checks make continuous feedback affordable, while human outer-loop reviews are budgeted at delivery boundaries and over long-term use.Machines may remind teams, gather evidence, and record verdicts, but cannot substitute for human judgment about whether the specification still fits the world.Source: §4.3 · p. 27

4.4 The severed backflow

  • Humans alone may amend the tradition: escaped defects must either enter the mechanized misfit enumeration or be explicitly ruled outside it with alternative coverage named.This severs the unsafe backflow from artifact repair to lawmaking while allowing routine repair to proceed without waiting for slow tradition changes.Source: §4.4 · pp. 27–28

4.5 The permanent novice

  • Observed compliance cannot establish that a generator has internalized a changing local tradition, so reliability evidence cannot warrant retiring artifact-level verification.Constraint compliance can degrade as constraints accumulate, and fine-tuning shows a shift in learned defaults rather than guaranteeing any particular subsequent output.Source: §4.5 · pp. 28–29
  • The harness remains a permanent external institution: human internalization may retire guidance, but not verification of each generated artifact.The tradition is consulted and enforced from outside the builder rather than possessed by it.Source: §4.5 · p. 29

5. Empirical Evidence

The case study repeatedly rebuilt a specified Scrum backend under a fixed end-to-end suite and evolving gates. Observations expose boundary escapes and detector drift, while the authors qualify what this single case establishes.

Case and rebuild process

  • All 64 problem-frame specifications across four aggregates were executed under the full gate stack, with the backend repeatedly rebuilt from empty source directories.Authors hand-wrote the first specification of each frame type, then used the model to generate later specifications from project materials and reviewed them.Source: §5 · pp. 30–31

Corpus and judgment

  • About 40,000 lines of YAML specifications exceed roughly 24,000 lines of generated production code; about half the specification lines are formatting and recurring structure, not new domain-semantic content.Many declarations record few new business decisions, and much use-case, contract, and initial acceptance material follows from aggregate definitions.Source: §5 · p. 30
  • About 27% of the corpus, roughly 11,000 lines, contained judgment-bearing scenarios, contracts, behavioral rules, and requirements; this share locates that material, not effort.The authors identify this as where the case's most substantial author judgment concentrated.Source: §5 · p. 32

Observation 1

  • Whole-aggregate verification found defects missed by per-artifact inspection, including unread inputs, unreachable error branches, lost derived state, and an unwired cross-aggregate reaction.The escapes exposed gaps in the misfit enumeration; they could prompt an enumeration change or an explicit ruling outside the mechanically gated set.Source: §5 · p. 32

Observation 2

  • Audits found stale rule counts, retired doctrine checks, silently narrowed scan sets, and stale documentation, showing that verification artifacts can drift too.The authors added checks against fixtures and real invocations to verify that rules still fire and are reached.Source: §5 · p. 33

Observation 3

  • Prompt-carried rules recurred across rebuilds and substituted same-family models, while corresponding gates caught violations; the model also drafted later pattern documents under author oversight.The model substitutions were working rebuilds, not controlled comparisons; authors retained authority over what gates checked.Source: §5 · p. 33

Empirical observations

  • Repeated rebuilds remained compatible with behavior exercised by the fixed end-to-end suite while the verification machinery continued to evolve.The authors characterize these observations as exercising the theory in operation, not as a benchmark evaluation.Source: §5 · pp. 30, 33

Scope and limitations

  • The single case does not establish portability, and individual measures of convergence, repair locality, loop cadence, and rule firing remain future work.PIT mutation scores measure test sensitivity to generated program mutations, not fidelity to acceptance scenarios.Source: §5 · pp. 32, 34

6. Answering Alexander’s Challenge

The paper answers Alexander’s generativity challenge by pairing a pattern language interpreted by the LLM with deterministic governance of its output. It formalizes coherence only as verifiable composition and reserves judgments about felt wholeness and whether the specification fits the world for people.

Generativity

  • The LLM and harness together make a written pattern language generative: specifications produce structurally uniform systems whose encoded obligations are verified, and the process can rebuild from empty directories.The LLM interprets the language; deterministic governance is needed because interpretation does not guarantee compliance.Source: §6 · p. 34

Coherence

  • Aggregate-wide, cross-frame, and cross-aggregate gates verify formal composition, but the paper does not claim to mechanize Alexander’s felt wholeness.The authors distinguish machine-checkable coherence from the structural, experiential quality Alexander describes.Source: §6 · p. 35

Habitability

  • The authors argue that enforcing the team’s encoded tradition preserves a shared architectural vernacular, while whether that structure is habitable remains an open question.They do not claim generated code is intrinsically easier to understand; that would require empirical study.Source: §6 · p. 35

The moral dimension

  • The assurance model locates the moral judgment in S = W, the relation between specification and world, which no machine verdict can discharge.The problem-side primary cannot be summoned into a test harness, and the authors note that reserving a slot for judgment is not yet an institution.Source: §6 · p. 35
  • A scheduled inhabitation review is proposed to record human judgments about the built world and feed findings back into amendments of the governing representations.The paper notes that non-engineer participation in Event Storming is not currently carried forward into formalization.Source: §6 · p. 35
  • Although the outer loop is slower and more expensive, the authors argue that routine machine checks should free human attention for the world-facing judgment that requires it.The engineer’s work therefore relocates to contact with the world and to building the tradition and harness.Source: §6 · pp. 35–36

7. Related Work

Related work supplies patterns, specifications, executable checks, and agent harnesses, but the paper derives a sufficiency theory for verification from Alexander’s account of fit and misfit. Its assurance remains conditional on an explicit enumeration, governed detectors, and human judgment where the world is concerned.

Specification and contract traditions

  • Problem frames, contracts, acceptance scenarios, domain-driven design, Clean Architecture, and mutation testing contribute components, but their conventional combination supplies no criterion for harness sufficiency.The paper’s misfit calculus addresses that question.Source: §7 · p. 36

Specification-driven work

  • Structured specification approaches govern artifacts and generation paths, while this theory asks what the verification boundary must establish before detected-misfit absence justifies fit.Specifications and detectors can misrepresent or drift from their sources, so the claim remains relative to identified and checked misfits.Source: §7 · pp. 36–37

Assurance cases

  • Assurance cases and eliminative approaches make confidence conditional on identified defeaters; this theory requires each enumerated misfit to have a live deterministic detector.That requirement enables adjudication at the rate candidates are produced.Source: §7 · p. 37

LLM code generation, repair, and guardrails

  • Coding benchmarks use externally supplied task oracles, whereas this theory targets systems generated from explicit specifications, where fit includes more than functional task completion.Self-repair methods can repair detected misfits inside the fix loop but do not determine which misfits gates should expose.Source: §7 · p. 37
  • Reflective agents optimize task performance, while the theory assigns humans the outer-loop judgment of whether specifications still fit the world; executable guardrails likewise do not establish sufficiency.The authors state that fit is only claimed against an explicit enumeration and escapes require extending, correcting, or explicitly ruling on it.Source: §7 · pp. 37–38

Repository-scale coherence and specification-driven verification

  • The paper distinguishes its specification-led checks from repository-derived specifications and self-consistency checks, and requires field-level tracing across representations.It also identifies the residual risk that passing existing checks does not cover requirements absent from the enumeration.Source: §7 · pp. 37–38

Harness engineering

  • Prior harness work studies interfaces, runtime responsibilities, automatic evolution, and evidence-gated agent loops; this paper derives harness obligations from Alexander’s theory of form.Its sufficiency claim is relative to the mechanized misfit enumeration, and changes to correctness norms require human-gated governance.Source: §7 · pp. 38–39

Design theory

  • The paper maps its theory to Gregor and Jones’s eight-component design-theory anatomy and claims novelty in deriving harness obligations from Alexander’s fit–misfit account.It models the LLM as a non-native vernacular builder whose pull toward mainstream idiom requires enforced tradition, detectable violations, and rules the builder cannot amend.Source: §7 · p. 39, Table 5 · p. 39

8. Limitations and Future Work

The evaluation leaves portability, builder variation, semantic test faithfulness, and the costs of harness construction unresolved. Future work also needs to extend verification across boundaries and establish institutions for human review of whether the system serves its users.

External validity

  • Evidence comes from one project and one solution family; portability remains untested and requires replication in a different binding.The proposed second-binding experiment holds the problem fixed while changing the architecture, technology stack, or implementation language.Source: §8 · p. 40
  • A different architecture would need its own schemas, decomposition units, pattern network, and gates, although the theory’s obligations are meant to stand.The evaluation selected a constraint-rich domain-driven, Clean Architecture, CQRS, event-sourced family; the alternative-family prediction is untested.Source: §8 · p. 40

Builder variation

  • Rebuilds did not isolate model capability, and all observed builders came from one model family, leaving cross-family violation profiles untested.The obligations attach to the builder premise rather than a particular model; telemetry could measure violation rates under a fixed law and harness.Source: §8 · pp. 40–41

Semantic faithfulness

  • S = T is the least directly verified relation: machines check test structure, not whether tests capture scenario meaning, so shared misreadings can pass.The multi-model semantic review remained advisory, and mutation scores cannot establish that tests assert the intended business rule.Source: §8 · p. 41
  • Proposed S = T remedies range from tracing expected values to assertions, through specification mutation, to deterministic test translation.Specification mutation is only advisory while LLM-generated tests make its verdict irreproducible; deterministic translation shifts trust to a translator that must itself be verified.Source: §8 · pp. 41–42

Verification coverage

  • Verification still has gaps within detector scans and across the frontend-backend contract, where field, date, and enum drift escaped local checks.Some gates can pass after silently narrowed or empty scans; cross-boundary drift was exposed only by end-to-end execution, while a deep comparison remains opt-in.Source: §8 · p. 42

Costs

  • Harness and specification effort, as well as the right amount of guidance content, remain unmeasured or unresolved.Harness effort is expected to be substantial, costs may amortize across repeated use, and guidance competes with generation for context-window capacity.Source: §8 · pp. 42–43

The outer loop

  • The human outer loop lacks institutions for scheduled inhabitation reviews, consistently recording intended beneficiaries, and non-engineer participation.These are identified as remaining design work needed to address whether the system continues to serve the people who live with it.Source: §8 · p. 43

9. Conclusion

Misfit-Governed Development derives harness obligations from Alexander’s theory of form under the premise of an unreliable builder. One working system shows that the obligations can be jointly discharged, while human judgment remains responsible for whether the specification fits the world.

9. Conclusion

  • MGD turns misfit enumeration into gates, tradition into a four-form pattern language, and vernacular repair into a regression-guarded fix loop.The builder proposes candidate forms, while enumerated misfits govern what may be accepted.Source: §9 · p. 43
  • One working system demonstrates joint feasibility of the derived obligations, while their discharge in other bindings remains to be tested.The obligations are derived from the classical theory under the changed builder premise; portability is not established by this case.Source: §9 · p. 43
  • The machine’s inner loop can be routine, leaving the human outer loop to judge whether the specification fits the world and software serves human life.Humans also approve extensions and amendments to the misfit enumeration.Source: §9 · p. 43

Availability

The paper distinguishes open-source supporting libraries from unreleased project-specific implementation and verification artifacts.

Availability

  • The ezddd libraries provide event-sourced domain-driven design and CQRS machinery for the solution-side language.They are open source.Source: Availability · p. 43
  • The uContract and ezspec libraries provide executable contracts and Given–When–Then scenarios for problem-frame specifications.They are open source.Source: Availability · p. 43
  • The reference implementation, specifications, and verification artifacts are not publicly released, so independent replication requires a new implementation of the stated obligations.The obligations are fully stated in the paper, and the second-binding experiment is specified at that level.Source: Availability · p. 43

Competing Interests

The authors disclose one competing-interest statement and describe the founder’s business and library-maintenance roles.

Competing Interests

  • Chien-Tsun Chen is the founder of Teddysoft, which offers training and consulting in domain-driven design, Clean Architecture, and AI-assisted software development.Source: Competing Interests · p. 44
  • The reference implementation’s open-source libraries are maintained under Chien-Tsun Chen’s GitLab account and published under Teddysoft’s package namespace.Source: Competing Interests · p. 44
  • Yu Chin Cheng declares no competing interests.Source: Competing Interests · p. 44

Generative AI Use Statement

The authors describe how AI tools contributed to implementation and manuscript preparation while reserving responsibility for the paper’s intellectual and editorial judgments to themselves.

Generative AI Use Statement

  • The authors developed the theoretical framework and methodology and retain sole responsibility for theoretical claims, decisions, interpretations, and final editorial judgments.Claude and other AI tools provided implementation, review, telemetry, and editing assistance under author direction.Source: Generative AI Use Statement · p. 44
  • Claude generated the reference implementation and, under author direction, later specifications, gate scripts, and pattern documents.Source: Generative AI Use Statement · p. 44
  • Claude, Gemini, and ChatGPT participated in optional multi-model review, while Claude and ChatGPT also provided manuscript feedback and English-language editing.Claude computed telemetry and corpus-composition figures for Table 3.Source: Generative AI Use Statement · p. 44

Appendix A. A Minimal Formal Vocabulary

Appendix A formalizes misfit-based fit, the agreement relations in S = P = T = W, and the detection-cost rationale for the dual-loop process. These formal claims remain bounded by the enumerated and successfully evaluated misfits, with world-fit reserved for human judgment.

A.1 Misfits and fit

  • A.1 fixes the governing representation during a repair window, enabling successive candidates to be judged against the same target.Amending that representation ends the window and re-enters through the legislature.Source: §A.1 · pp. 44–45
  • A.1 makes fit relative to the finite misfit enumeration and to the subset a run successfully evaluates, so an unevaluated detector cannot count as a pass.A fit report must establish that all enumerated predicates were evaluated; otherwise it overstates what was checked.Source: §A.1 · p. 45
  • A.1 treats governing representations and detector checks as preconditions for trusting a fit verdict, not as additional misfit predicates.Representation checks include specification syntax and semantics, proxy-to-primary reconciliation, determinism, and detector fixture and reachability checks.Source: §A.1 · p. 45

A.2 The semantics of S = P = T = W

  • A.2 defines S = P = T = W as agreement relations, not identity, between the specification, program, tests, and world.The machine-decidable portion compares declared elements with program and test artifacts; tradition is checked separately.Source: §A.2 · p. 46
  • A.2 checks structural realization of declared elements, acceptance-scenario test coverage, and passing tests across configured infrastructure profiles.Undeclared domain-event fields and aggregate public behavior methods are blocking, while other undeclared realizations are advisory.Source: §A.2 · p. 46
  • A.2 limits scenario coverage to scenarios not deferred by the specification, and acknowledges that structural test matching does not establish deeper faithfulness.A specification may defer tests for an entire tier, such as integration tests.Source: §A.2 · p. 46
  • A.2 leaves S = W to lived use and stakeholder judgment because the world’s demands lack a complete machine-verifiable representation.The three machine-decidable relations make sustained human attention to world-fit affordable, the theory’s economic claim.Source: §A.2 · p. 46

A.3 The detection-cost bound

  • A.3 distinguishes machine-priced detection, frequent enough for artifact changes, from human-priced detection, which must be scheduled less frequently.The difference in affordable feedback cadence motivates the dual-loop architecture.Source: §A.3 · p. 47
Loading 2610.01372v1…