Skip to content

CONCEPT Cited by 4 sources

Specification-driven development

Definition

Specification-driven development is a workflow where the specification is a first-class, authored, maintained artifact — produced early, visible to customers, and continuously validated against implementation and/or model outputs. It contrasts with the historical norm where specs were produced once, discarded, and never re-consulted, and with implicit/tacit specs that live only in reviewer heads.

The spec can be textual, formal, temporal, or executable (patterns/executable-specification), but the defining property is customer-visibility and active maintenance.

Why this concept emerges now

Two structural shifts force specs to the surface:

  1. Agentic AI has no implicit spec. A pre-AI code review assumed the spec lived in the reviewer's head. An agent has no head. The envelope around what the agent may and may not do must be written down for the automated reasoner to check it (patterns/envelope-and-verify).
  2. Neurosymbolic tooling made specs enforceable. Pre-2020, a formal spec was an expensive artifact with a narrow audience (TLA+ specialists, theorem-prover authors). LLM front-ends + concepts/automated-reasoning backends make specs a much cheaper input with a much larger audience — and make the verification on the other end mechanical.

There are numerous specification languages and concepts... I'm excited to see customers discover these concepts and begin demanding them of their specification-driven tools. — Byron Cook (Source: sources/2026-02-17-allthingsdistributed-byron-cook-automated-reasoning-trust-ai)

Productized surfaces

  • systems/kiro — AWS's specification-driven development tool; Cook names it as one of the two flagship customer-facing vehicles for making specifications mainstream.
  • systems/bedrock-guardrails-automated-reasoning-checks — lets customers author a specification and have Bedrock mechanically verify AI outputs against it, with up to 99% provable accuracy.

Dimensions customers will have to learn

Cook's prediction: the customer-visible specification surface will broaden. Concrete dimensions:

  • Branching-time vs linear-time temporal logic (CTL* vs LTL): does the spec describe a single timeline or a tree of possible timelines? (See concepts/temporal-logic-specification.)
  • Past-time vs future-time operators: "was there ever a state where X held?" vs "will X always hold?"
  • Logic of knowledge and belief (epistemic): "the agent knows fact F", distinct from "F is true"; required for multi-agent reasoning where what each party knows drives behavior.
  • Causal reasoning: A caused B, distinct from A correlates with B.

These are not exotic — they are the 50-year-old vocabulary of formal-methods research. What changed is that customers now need them.

Autoformalization is the bottleneck

The single biggest obstacle Cook names to making specification-driven development mainstream: autoformalization — translating natural-language intent into formal specifications. Today, writing a formal spec still requires specialist skill. Collapsing that gap is the active research frontier:

  • DARPA's expMath program.
  • systems/kiro's spec-authoring UX.
  • Bedrock Guardrails' reasoning-checks spec inputs.

Until autoformalization is solved at the end-customer level, specification-driven development is gated on someone-with-training-writing-the-spec. Progress is visible and fast.

The deeper problem: humans rarely agree on specs

One thing specs surface that was invisible before: subtle contradictions in the rules themselves. Cook cites: - Amazon internally trying to nail down AWS policy semantics. - Internal debate over virtual-network semantics. - Copyright law simultaneously requiring "original intellectual creation" and protecting works with no creative human input.

Specifications expose rule conflicts because they force the rule to be stated explicitly and completely. This is a feature for engineering correctness — the time to discover your spec is contradictory is before you deploy, not after — but it means spec-authoring surfaces political/organizational/legal conflict that was previously tacit.

Relation to executable specification

patterns/executable-specification is a specific flavor of specification-driven development: the spec is written as code, in the same language as production, checked into the same repo, and validated via property-based testing against production (ShardStore is the canonical case). Spec-driven development is the broader workflow; executable specs are one materialization of it.

Other materializations: - Temporal-logic specs for agentic-system envelopes (patterns/envelope-and-verify). - Constraint specs for post-inference filtering (patterns/post-inference-verification). - Policy specs for security (systems/aws-policy-interpreter).

Seen in

Last updated · 200 distilled / 1,178 read