Claim-Driven Development

A specification for a development workflow where the unit of work is the claim: a checkable promise about what a function does. Not the test, and not solely the source code, but the reasoning behind the intent of the code and its region of validity. The level of trust to be put on the correctness of code is proportional to the weight of evidence behind it.

The problem this is for

Writing code used to be the hard part, and reviewing it was comparatively easy: a human read a diff, recognized the pattern, and trusted it because (a) they understood it fully or (b) moslty understood it but knew and trusted the author. This has changed substantially over the past few years with the emergence of AI.

A model can now readily write a correct-looking package (with a suite of test files and documentation), in less time than it takes to write a single correct function manually. Generating plausible and highly tested code is no longer the hard part. In fact the ease of generation may have already become a new problem, because how do you end up trusting what is generated?

Reviewing the output of code development to a high standard has become the bottleneck and a likely point of failure. A human now has to decide whether to trust code they are ultimately less familiar with and where they have limited ability to gauge the expertise of the code generating model.

Increasingly code will not be read line by line, and "passing tests" is weak evidence when the tests themselves were written by the same process that wrote the code, with the same biases and blind spots.

The real thing that used to make code trustworthy: a person with sufficient expertise understanding and verifying it (usually by writing unit tests to express their intent), doesn't scale to agentic code development practices.

With the rise of generative code development workflows, we're faced with an age old problem, namely that language is imprecise for defining intent and instead CDD reaches for something more mathematical to solve this.

CDD is aimed to reduce these exact gaps: it separates out stating what must be true about a function from the actual writing of the function itself, so the thing a human reviews is a relatively short list of properties (the knowledge base), not solely an implementation. The part that gets checked mechanically is whether the implementation has actually implemented those properties correctly, via running it in a CI pipeline and iterative development loop, not by unwarranted trust.

The loop

1. State claims first. Written by a human, or proposed by an agent for a human to look over. A claim starts as a conjecture either way.
2. Implement, or generate. The claim set plus the intent describes what the function must satisfy, informing an implementation the way a test suite already does in TDD, whether a human writes the function by hand or a model generates it. CDD doesn't assume AI wrote the code, and it doesn't replace an existing test suite: ordinary tests still pin concrete regressions, claims add implementation-independent laws on top.
3. Verify. Each claim is checked against the real implementation: holds (n=...) under seeded testing, or falsified with a counterexample kept permanently.
4. Diagnose. A falsified claim has exactly two possible causes: either the implementation is wrong, and the counterexample drives another pass through step 2, or the claim was wrong, resulting in a discovery about the problem rather than a defect in the code.
5. Retain as new knowledge. A claim diagnosed as a genuine discovery is kept as new recorded knowledge.
6. Accept. Once every claim has been adjudicated, (proved or falsified), any implementation that re-verifies the same claim set is trusted the same as the one before it; a later regeneration re-enters the loop at step 2, and the counterexamples already on record make it also a regression check.

Full definition, including who typically does each step and a diagram of the cycle: v0.2.0/cdd.md.

Why not an existing verification approach

Every individual mechanism CDD makes use of has precedent; the combination and the role it plays are what's different.

• Design by Contract / refinement types (Eiffel, deal, icontract, Liquid Haskell, Dafny): contracts check the inputs that happen to occur at runtime, or require the code to be written in a way a prover accepts.

  CDD claims are verified across the declared domain before acceptance, not wherever the code happens to be called from, and don't require rewriting the implementation to satisfy a proof assistant.

• Property-based testing (QuickCheck, Hypothesis):

  CDD builds directly upon property based testing, but treats the property as the primary artifact of development instead of a testing technique applied after the fact.

  The claim set is normally stated before the code (and informs the generation prompt if AI is used), not a check on code that already exists, though claims can just as well be retrofitted onto code that predates them; CDD doesn't require greenfield. A claim's statement (see v0.2.0/declared-schema.md) can be written in whatever expression grammar a tool defines, including one that's a superset of an existing property-testing library's own property language, so adopting CDD doesn't require throwing away properties already written for QuickCheck or Hypothesis.

• Invariant inference (Daikon, QuickSpec): these discover likely invariants from execution traces.

  CDD's claims are stated with intent, human- or model-proposed, then adjudicated; the verifier never trusts its own inference, and a proposer never adjudicates its own claims.

• BDD (Cucumber/Gherkin): scenarios are still worked examples, concrete inputs and outputs.

  Claims are statements, quantified over a domain, not example cases.

• Data contracts (dbt tests, Great Expectations): these make claims about a dataset in its current state.

  CDD's claim anatomy generalizes this (domain, statement, tolerance, evidence route) to arbitrary functions, not only tabular data.

• Content-addressed code (Unison): identity by hash instead of by name or file location, within one language.

  CDD borrows this identity move (rename-invariant form hash) but binds it to evidence, not only to storage: two implementations with the same verified claim set can be treated as the same function even if their hashes/implementations differ (assuming sufficient claim coverage).

What's actually new is the composition: claims can be stated before generation/implementation, as the compilation contract for what's intended, bound to a rename-invariant identity, explicitly designed for a world where the implementation will change rapidly and easily, but where oversight becomes increasingly difficult. Nobody needed that combination until code files stopped having a single, known, trusted author.

What's in this repo

Each published version has its own directory, immutable once released. v0.2 is current; v0.1.0 remains for records that conform to it (a record's lineage.CDD_spec_version says which to read it against).

• v0.2.0/cdd.md: the workflow, the epistemic rules ("say what you know, and no more", the executed-witness rule for falsification), additive-only vocabularies.
• v0.2.0/claim-anatomy.md: the claim structure (domain, statement, tolerance, evidence route, premise).
• v0.2.0/record-schema.md: the small normative core two tools must agree on, and everything the spec deliberately leaves implementation-defined. Claim identity belongs to the grammars.
• v0.2.0/declared-schema.md: the YAML shape for proposing a claim set, before anything is checked, including premises and typed claim dependencies.
• v0.2.0/verified-schema.md: the YAML shape a conformant tool writes after checking one, including the authored object, acceptance, records-have-memory, and freshness composition.
• v0.2.0/evidence-ladder.md: the verdict vocabulary (unknown and invalidated join in v0.2), the stance fold, strict vs lenient.
• CHANGELOG.md: spec versions, on their own cadence, independent of any implementation's release schedule.

Implementations

Intentionally none are bundled with this spec: there is no code in this repo, and no implementation is privileged by these documents. Any tool, in any language, that reads and writes the record shape defined here conforms.

The first tool (in development) against this spec is mathema, a downstream python project. Nothing in this spec depends on it or assumes its choices.

Contributing

Contributions are welcome and go through an ordinary pull request. With your first one, state in the PR description that you accept the Contributor Licence Agreement; one sentence is enough, no tooling involved. The agreement is a licence grant, not an assignment, it never limits what you do with your own work, and its section 3 means your contribution can never be relicensed into anything closed: the specification's stay-open promise binds the maintainer too, the same way ShareAlike binds everyone else. What it adds over the licence alone is a patent grant (which Creative Commons licences exclude) and the ability for the specification to move to another open home, a standards body, say, without hunting down every past contributor.

License

The documents in this repo are CC BY-SA 4.0: reuse and adapt freely, with attribution, and a derivative of the specification stays open under the same terms. That's deliberately a different kind of license from whatever an implementation might use for its code (a software license, or a source-available one); the spec for CDD is meant to be able to move independently from any implementations, and ShareAlike is what keeps a fork of the spec itself from being closed.