Follow-up to "Spec-driven development is half the loop"
A reviewer raised this question after reading the draft:
Some practitioners argue that spec-level properties (interface contracts, invariants) live at a different level than tests and oracles and deserve to be considered verification in their own right.
The main post hand-waves this by drawing a hard line between "mechanical oracle" and "soft oracle." That line is real, but a reviewer has a point that it's not binary — specs live on a continuum.
Scope
- The continuum: prose requirement → structured requirement → type signature → executable contract → mechanically-discharged contract → proof term
- At what point does the artifact earn the word "verification"?
- Concrete examples from our stack: Verus contracts in gale, Rocq refinement proofs, rivet schema rules, sigil attestation predicates
- Counter-examples: what soft specs mask that mechanical ones don't
- Implications for SDD tools: the minimum structure a Spec Kit / Kiro output needs to cross the threshold into verification
Target
1500–2000 words, depth post. Prior art: Formal verification just became practical.
Source
Part of the review on content/blog/2026-04-23-spec-driven-development-is-half-the-loop.md (currently draft). Deferred from that post as "too deep for this one."
Follow-up to "Spec-driven development is half the loop"
A reviewer raised this question after reading the draft:
The main post hand-waves this by drawing a hard line between "mechanical oracle" and "soft oracle." That line is real, but a reviewer has a point that it's not binary — specs live on a continuum.
Scope
Target
1500–2000 words, depth post. Prior art: Formal verification just became practical.
Source
Part of the review on
content/blog/2026-04-23-spec-driven-development-is-half-the-loop.md(currently draft). Deferred from that post as "too deep for this one."