Verified Spec-Driven Development (VSDD)

Comments

Verified Spec-Driven Development (VSDD)

The Fusion: VDD × TDD × SDD for AI-Native Engineering

Overview

Verified Spec-Driven Development (VSDD) is a unified software engineering methodology that fuses three proven paradigms into a single AI-orchestrated pipeline:

• Spec-Driven Development (SDD): Define the contract before writing a single line of implementation. Specs are the source of truth.

• Test-Driven Development (TDD): Tests are written before code. Red → Green → Refactor. No code exists without a failing test that demanded it.

• Verification-Driven Development (VDD): Subject all surviving code to adversarial refinement until a hyper-critical reviewer is forced to hallucinate flaws.

VSDD treats these not as competing philosophies but as sequential gates in a single pipeline. Specs define what. Tests enforce how. Adversarial verification ensures nothing was missed. AI models orchestrate every phase, with the human developer serving as the strategic decision-maker and final authority.

I. The VSDD Toolchain

**************************

II. The VSDD Pipeline

****Phase 1 — Spec Crystallization****

Nothing gets built until the contract is airtight — and the architecture is verification-ready by design.

The human developer describes the feature intent to the Builder. The Builder then produces a formal specification document for each unit of work. Critically, this phase doesn't just define what the software does — it defines what must be provable about it and structures the architecture accordingly.

Step 1a: Behavioral Specification

The Builder produces the functional contract:

• Behavioral Contract: What the module/function/endpoint must do, expressed as preconditions, postconditions, and invariants.

• Interface Definition: Input types, output types, error types. No ambiguity. If it's an API, this is the OpenAPI/GraphQL schema. If it's a module, this is the type signature and doc contract.

• Edge Case Catalog: Explicitly enumerated boundary conditions, degenerate inputs, and failure modes. The Builder is prompted to be exhaustive here — "What happens when the input is null? Empty? Maximum size? Negative? Unicode? Concurrent?"

• Non-Functional Requirements: Performance bounds, memory constraints, security considerations baked into the spec itself.

Step 1b: Verification Architecture

Before any implementation design is finalized, the Builder produces a Verification Strategy that answers: "What properties of this system must be mathematically provable, and what architectural constraints does that impose?"

This includes:

• Provable Properties Catalog: Which invariants, safety properties, and correctness guarantees must be formally verified — not just tested? Examples: "This state machine can never reach an invalid state." "This arithmetic can never overflow." "This parser always terminates." "This access control check is never bypassed." The Builder distinguishes between properties that should be proven (critical path, security boundaries, financial calculations) and properties where test coverage is sufficient (UI formatting, logging, non-critical defaults).

• Purity Boundary Map: A clear architectural separation between the deterministic, side-effect-free core (where formal verification can operate) and the effectful shell (I/O, network, database, user interaction). This is the most consequential design decision in VSDD — it dictates module boundaries, dependency direction, and how state flows through the system. The pure core must be designed so that verification tools can reason about it without mocking the entire universe.

• Verification Tooling Selection: Based on the language and the properties to be proven, the Builder selects the appropriate formal verification stack (Kani for Rust, CBMC for C/C++, Dafny, TLA+ for distributed systems, etc.) and identifies any constraints these tools impose on code structure. This happens now, not after the code is written, because tool constraints are architectural constraints.

• Property Specifications: Where possible, the Builder drafts the actual formal property definitions (e.g., Kani proof harnesses, Dafny contracts, TLA+ invariants) alongside the behavioral spec. These aren't implementation — they're the formal expression of what the spec already says in natural language. They serve as a second, mathematically precise encoding of the requirements.

Why this must happen in Phase 1: If the system is designed with side effects woven through the core logic, no amount of Phase 5 heroics will make it verifiable. A function that reads from a database, performs a calculation, and writes to a log in one block cannot be formally verified without mocking infrastructure that the verifier may not support. But a function that takes data in, returns a result, and lets the caller handle persistence — that's a function a model checker can reason about. This boundary must be drawn at the spec level because it fundamentally shapes the module decomposition, the dependency graph, and the testing strategy that follows.

Step 1c: Spec Review Gate

The complete spec — behavioral contracts and verification architecture — is reviewed by both the human and the Adversary before any tests are written. Sarcasmotron tears into the spec looking for:

• Ambiguous language that could be interpreted multiple ways

• Missing edge cases

• Implicit assumptions that aren't stated

• Contradictions between different parts of the spec

• Properties claimed as "testable only" that should be provable (the Adversary pushes back on lazy verification boundaries)

• Purity boundary violations — logic marked as "pure core" that actually depends on external state

• Verification tool mismatches — properties the selected tooling can't actually prove

The spec is iterated until the Adversary can't find legitimate holes in either the behavioral contract or the verification strategy.

Chainlink Integration: Each spec maps to a Chainlink Issue. Sub-issues are generated for each behavioral contract item, edge case, non-functional requirement, and each formally provable property. The provable properties get their own bead chain so their status is tracked independently from test coverage.

****Phase 2 — Test-First Implementation (The TDD Core)****

Red → Green → Refactor, enforced by AI.

With an airtight spec in hand, the Builder now writes tests — and only tests. No implementation code yet.

Step 2a: Test Suite Generation

The Builder translates the spec directly into executable tests:

• Unit Tests: One or more tests per behavioral contract item. Every postcondition becomes an assertion. Every precondition violation becomes a test that expects a specific error.

• Edge Case Tests: Every item in the Edge Case Catalog becomes a test. These are the tests that catch the bugs that "never happen in production" (until they do).

• Integration Tests: Tests that verify the module works correctly within the larger system context defined in the spec.

[...]

Original source