SpecArtisan: Turning Requirements into Verifiable Contracts for AI Coding Agents

In AI-assisted development, requirement understanding deviations often surface late — during integration rather than at first code generation. A music player example illustrates this: the UI may show a pause icon while audio fails to play, or the progress bar advances despite load failure. These mismatches between requirements, design, code, and reports make root-cause localization difficult.

From Requirements to Traceable Contracts

SpecArtisan converts raw requirements into a verifiable design contract ( specartisan.yaml) before the agent writes code. It decomposes requirements into modules, APIs, end-to-end cases, exception branches, UI behaviors, and acceptance checkpoints — each with a stable ID traceable to implementation files and tests.

For the music player, a vague "click button → call play()" becomes a contract with explicit pre/post conditions and branch scenarios:

hoare_contract:
  pre_condition:
    - "music_player.playbackState in {IDLE, PAUSED, ERROR}"
  post_condition:
    - "result.isSuccess implies playbackState == PLAYING"
    - "result.isSuccess implies progressTimer.running == true"
  branch_scenarios:
    - branch_id: BRANCH-PLAY-FAILED
      post_condition:
        - "playbackState == ERROR"
        - "progressTimer.running == false"
      ui_logic:
        - 'OnFailure → Toast.setMessage("播放失败，请重试")'

This makes deviations detectable: premature button switching or a still-running progress bar after failure become locatable violations. The same rigor applies to permission errors, empty states, duplicate operations, concurrency conflicts, and technical failures — each must be an explicit branch, not hidden in notes.

An internal retrospective of 56 early practice issues showed recurring first-round omissions, lost precise values, and vanished exception branches. The root cause was not that the agent missed the text, but that no stable structure forced it to retain every commitment. SpecArtisan retains commitments first.

From Structured Specs to Evidence-Gated Verification

Writing contracts in YAML is only step one. Without checking, structured docs can drift, miss items, or align neatly with wrong code. SpecArtisan's second pillar gates the spec through verification.

Mechanical verification checks required structure, ID uniqueness, reference resolution, module dependency cycles, UI component types, affected files, and traceability. These are deterministic: missing references error, dependency cycles block, unregistered UI operations halt. Semantic and Hoare verification then handles behavioral parts.

Returning to the music player, playback, pause, and load failure must form a coherent state-transition group, not disconnected booleans:

Click play: IDLE / PAUSED / ERROR → LOADING

Load success → PLAYING with timer running

Pause retains current position

Load failure → ERROR, timer stops, play icon restores

Verification requires the report to locate real code entry points and state mappings, then walk the call chain: which play method handles the click, where the audio engine's success callback sets PLAYING, who stops the timer on failure. A play() method existing does not equal music playing; unmapped entries are marked MAPPING_BLOCKED, unclosed evidence chains yield UNKNOWN, and counterexamples are explicitly VIOLATED. These verdicts, though less pretty than PASS, carry more diagnostic value.

Four Core Artifacts and Cross-Role Alignment

A full run produces four artifacts: the design contract ( specartisan.yaml), a requirement coverage report, a structure and semantic check report, and a contract-code reasoning evidence report. Product, design, development, and test no longer hold separate descriptions; they collaborate around one contract, discussing whether a requirement entered design, whether code truly carries it, and whether the gap is missing implementation or missing evidence.

Scope and Limitations

SpecArtisan is a semi-formal method. It does not replace compilation, automated testing, or real-device acceptance, nor does a single YAML automatically comprehend an entire legacy codebase. The authors retain this boundary because a reliable tool must first know what it has not yet proven.

Getting Started

Load the Skill from the repository's .github/skills into a common IDE or CLI to run agents under SpecArtisan's workflow. A small feature like the music player — covering play, pause, load failure, and state transitions — is sufficient for a first trial. Observe whether the agent's response shifts from "code is done" to "every commitment, I can show where it landed." Code can be generated; design must not rely on guesswork.