The Closure
field guide.

A definition of complete software that a repository can be checked against, and the procedure that checks it.

Definitions first, then procedure. Everything here is decided on your machine against a checkout, whether your agent asks or you type the command. The walkthrough at the end shows one recorded run on the fixture Closure ships with; the interactive report there illustrates the same model with authored data and does not read a repository.

What complete means

Software used to finish when the next change stopped being worth its cost. Once a coding agent can always produce one more change, finishing needs a definition that does not depend on anyone getting tired. This is the one Closure evaluates.

Software is complete, for a declared scope at a particular commit, when everything the scope owes up to its declared targets is proven by admissible evidence that still matches the repository, and nothing about the scope is left unresolved.

Every term in that sentence is decided by a rule rather than a judgment. In the order a reader needs them:

Scope: What you say the product owes: the capabilities you select from a versioned, human-authored catalog, with their parameters, exclusions, and a target level for each. Completion is only ever relative to a scope, and a scope that owes nothing cannot be complete.
Owed: Every obligation the scope implies once the catalog’s dependencies and policies are followed to a fixed point. An obligation is one falsifiable statement about observable behavior, with the evidence that would settle it named in advance. “Teams can invite people” owes token entropy, expiry, revocation and cross-tenant guards whether or not anyone thought of them.
Target: A capability’s obligations sit on a ladder of five tiers, and its target names the rung it must reach. Obligations above the target are the next rung, not an outstanding debt.
Proven: An obligation is proven when it holds evidence of a kind it accepts, whose inputs were recomputed against the repository and still match. Evidence that is merely claimed, stale, inadmissible or absent does not count, and there is no partial credit.
At a commit: Every proof records a digest of what it depended on. The verdict is a property of the repository at that commit, not of the run that reported it, and it moves when the facts do.
Unresolved: Expansion can reach a decision it is not allowed to make: an ambiguous concept, two features that want the same parameter set differently, a required feature the scope excluded. Each becomes a gap that blocks completion until a person settles it, as does any request to weaken or drop a requirement.

The ladder.

Tiers order the work so that every capability exists before any capability is polished. A small set of invariants whose retrofit cost is a rewrite, such as tenant isolation, is hoisted into the first rung.

ExistenceThe path exists and has been observed to execute end to end, once.
Happy pathSpecified behavior on well-formed input is verified.
FailureNamed failure modes produce specified behavior.
InvariantSecurity, isolation, idempotency and authorization hold as properties.
OperabilityObservability, degradation, recovery and data lifecycle.

What’s owedExpanded requirements

What’s provenAdmissible evidence

What’s leftThe remaining plan

plan = closure(selected concepts, pinned catalog)
       − satisfied(observed system)

The level is a floor.

A capability’s level is the highest rung at which it and every rung below are fully proven, counting only rungs the catalog populated. The product’s level is its lowest capability. A polished corner cannot raise the number, and thinning the catalog cannot either: a capability targeted deeper than its catalog entry goes is an authoring gap, and it blocks completion.

The definition and the grading are deterministic. The same catalog version, scope and commit give the same obligation set and the same verdict, whoever wrote the code. The code that satisfies them does not have to be.

What counts as proof

Each obligation names the kinds of evidence it accepts, in order of strength: a business path traced end to end, a live probe, a property or example test, a contract or schema, a registered route, or, for something no tool can check, a signed human attestation with a scope and an expiry. A route existing and a route behaving correctly are different claims, so admissibility follows the claim rather than the label on the evidence. Static evidence proves a structural claim at full strength and a behavioral claim only at a disclosed fallback strength.

PROVEN: Admissible evidence whose inputs digest was recomputed against the repository and still matches. The only state that counts.
CLAIMED: Admissible evidence that nothing has independently recomputed. A record asserting its own digest is worth nothing until something checks it, so it never counts toward a level.
STALE: The inputs changed, so the old proof no longer establishes the current state. Equivalent to unproven, logged differently.
INADMISSIBLE: Evidence that fails the obligation’s acceptance rules: the wrong kind, or test evidence without a valid negative control.
UNPROVEN: No supporting evidence, or evidence that records a failure.

Proof has a shelf life.

The digest covers what the proof depended on: the files the test executed, the extractor that read the result, the wording of the obligation it answered, and the perturbation declared to check it. A mismatch reopens the obligation rather than preserving a misleading green status. Regression becomes a scheduling event, not a discovery.

PROVENThe proof’s inputs match

STALEA covered input changes

Verify againReconcile fresh evidence

Changed inputs reopen the obligation. Yesterday’s proof is not today’s verdict.

Two strengths.

Primary evidence is the kind the obligation asked for, checked by the harness. Fallback evidence satisfies the obligation by weaker means: static evidence for a behavioral claim, a test that CI never runs or conditionally skips, or a negative control the worker reported rather than the harness observed. Fallback proofs are counted on their own line in the plan and the verdict, and the release check refuses them.

Which languages and report formats work?

Evidence is language-neutral. Closure reads the report your runner already writes: the Jest JSON shape, JUnit XML, Go’s test events, TRX and RSpec JSON, which covers Vitest, Jest, node:test, pytest, go test, cargo, Maven and Gradle, dotnet test, PHPUnit, RSpec and Minitest. A test’s dependency set comes from the import graph for TypeScript and JavaScript and from a coverage trace for everything else, so a proof decays when the code the test executed changes, whatever language it is written in.

Negative controls

A passing test proves that every assertion someone wrote still holds. It does not prove the assertions reach the behavior the obligation names. For critical and tier-4 test evidence, a passing test alone is inadmissible: the harness must have watched the named test fail when the mechanism it claims to protect is removed.

Prepare an isolated copy of the repository.
Run the one named test and establish that it passes.
Apply the declared perturbation to the mechanism under test.
Run the same test again and observe whether it fails.

After the declared perturbation

The same test failsSensitivity demonstrated: The named test notices the chosen change. That is what this control establishes.
The same test still passesSensitivity not demonstrated: Investigate the control. The perturbation may have missed the intended protection.

A passing test after perturbation does not demonstrate sensitivity to that mechanism. A test that fails before perturbation establishes nothing about the control. A control that the worker merely reports is not equivalent to one the harness has verified. And the harness grades the one test the control names, not the file it lives in: a perturbation that breaks a neighbouring test is not a control for this one.

Evaluating a repository

Closure runs locally against a checkout, in any language whose test runner can write a report. Install the package file delivered with your purchase (or the Claude Desktop extension; see setup for each app), then take the shipped example first: it contains a test that passes while the behavior is wrong, and a walkthrough from that test to a verified repair.

npm install --global ./closure-engine-0.2.3.tgz
closure demo --out closure-demo

For your own repository, inventory it and initialize a scope:

closure scan --repo ../subject
closure init --repo ../subject

That detects the test components (JavaScript and TypeScript, Python, Go, Rust, Java and Kotlin, C#, PHP and Ruby) and writes into the subject’s own .closure/:

selection.yaml: Where you say what the product owes, and to what target. Starts empty: a scan can inventory an implementation, but it cannot decide what your product should do.
binding.yaml: How to run one test, how to run it under coverage, where the report lands, and how a test names the obligation it proves.

It never overwrites either. A components.json records the detected build roots and runners.

From the first selection to the next task.

Say what is owed.
Choose capabilities and a target for each. A verdict over nothing is refused.
```
$EDITOR ../subject/.closure/selection.yaml
```
Run the suite and write the report.
doctor checks toolchains without running project code. test runs the native runner and writes the normalized report that observe reads. Running a subject’s tests needs its own dependencies and services; Closure never installs them.
```
closure doctor --repo ../subject
closure test   --repo ../subject
```
Observe, plan, and read the verdict.
observe reads the report and the repository and never runs a suite. plan is what is owed minus what is proven, by capability and tier. done is the predicate, clause by clause, with the count blocking each.
```
closure observe --repo ../subject
closure plan    --repo ../subject
closure done    --repo ../subject
```
Take the next obligation.
A task envelope for whoever writes the code, person or agent: the requirement, why it is owed, exactly what proof will be accepted, and what the worker may not touch. Name its test with the selector init chose.
```
closure next --repo ../subject
```
Trace the proof’s dependencies.
Runs each bound test under coverage and records the files it executed, so the proof decays when they change.
```
closure trace --repo ../subject
```

That is one pass, and the envelope is its unit of work. Whoever takes it lands the change and names its test with the selector chosen at init. Run test, observe and done again: the obligation becomes proven only if its evidence survives the digest check, and any proof whose files the change touched goes stale and returns to the plan on its own. Repeat until done holds, then apply the release bar below.

With the subject’s own files in place, --repo is the only flag any command needs. observe only reads. test, trace, mutate and verify-control run tests, the last three always in an isolated copy.

Verifying a declared control

closure mutate         --repo ../subject <obligation> --write
closure verify-control --repo ../subject <obligation>

The search proposes a perturbation the named test notices, in JavaScript, Python or Go today; the harness applies it in a scratch copy and grades the one test the control names, not the file it lives in. Review a proposal against the obligation before accepting it: a kill in a large file is often incidental.

The DONE predicate

closure done evaluates the definition above as ten clauses and prints each with the count blocking it, because “not done” is useless and “not done, four obligations unproven, one of them stale” is a plan. Grouped by what they protect, the conditions are:

The scope is valid.Something is owed, and no capability is targeted deeper than its catalog entry specifies.
The obligation set is settled.Expansion reached a fixed point with no unresolved gap, no contested obligation, and no blocking provisional one.
Required proof is present.Every obligation at or below its capability’s target is proven, none rests on claimed evidence, and every capability reaches its target level.
Every required scenario traverses end to end.A declared business path across capabilities is one obligation, proven only by running it.
Nothing is waiting on a person.No request to weaken or exclude a requirement is pending. These are the only changes a human must approve; everything else the engine derives.

What a verdict looks like: the fixture Closure ships with, its satisfied clauses folded away. The full ledger is in the walkthrough below.

DONE(example-saas)  =  FALSE

  + something is owed
      58 obligations selected
  x [32] every obligation required at the declared targets is proven
      32 unproven, of which 0 inadmissible and 2 stale
  … 1 satisfied clause omitted
  x [7] every capability reaches its target level
      AUDIT.EVENTS T0/T1, BILLING.SEAT_ACCOUNTING T0/T1, COLLAB.INVITATION T0/T3, EMAIL.DELIVERY T0/T3, IDENTITY.ACCOUNT T0/T4, ORG.MEMBERSHIP T0/T1, SCENARIOS T0/T1
  x [3] every required scenario traverses end to end
      0 of 3 traversable
  … 5 satisfied clauses omitted
  ~ [3] advisory: proofs at full strength
      3 proven at fallback strength (weaker kind, partial surface, or self-attested control)

Blocked on: every obligation required at the declared targets is proven
This verdict is a property of the repository at this commit, not of this run.

Done and release are different bars.

done may pass with fallback proofs and lists them as an advisory. release-check adds two clauses: every required proof at primary strength, and every required control with a current verification receipt. A refused control, a stale receipt, or one the worker reported rather than the harness observed blocks a release. After code changes, verify again.

closure release-check --repo ../subject

DONE = TRUE means the declared scope is satisfied at this commit by evidence the engine could check. It does not mean bug-free, safe, or finished in any sense the scope did not declare. The catalog can miss a requirement, an extractor can have limited reach, and human review can find what the inputs do not describe. Closure gives you an explicit, inspectable stopping condition and names exactly which inputs it rests on.

One repository, end to end

Everything in this section was recorded from one run of the engine on the fixture it ships with, a small SaaS app built on Next.js and Postgres. The homepage shows excerpts; this is the whole of each output, followed by two illustrations of the parts a first verdict cannot show.

The plan

One sentence was selected: teams can invite people. plan resolves it to a catalog feature, follows that feature’s dependencies and policies to a fixed point, and prints what is owed minus what is proven, by capability and tier.

verifier  digests recomputed from fixtures/example-saas

PLAN  example-saas                  profile ts-node-postgres
catalog  closure-profile@0.1.0 saas-core@0.1.1catalog hash eb59d29719
graph    5f7285fa42                 floor 1
scope    6 features, 6 resources, 58 obligations

CONCEPTS
  "teams can invite people"                  -> COLLAB.INVITATION@3.1.0     [CONCEPT.INVITE_PEOPLE]

DERIVED FEATURES (5 added by closure, no approval required)
  + AUDIT.EVENTS@1.0.0              <- BILLING.SEAT_ACCOUNTING@0.3.0  seat changes affect what a customer is…
  + BILLING.SEAT_ACCOUNTING@0.3.0   <- COLLAB.INVITATION@3.1.0  seat limits must be enforced against an auth…
  + EMAIL.DELIVERY@0.4.0            <- COLLAB.INVITATION@3.1.0  invitations are delivered out of band and th…
  + IDENTITY.ACCOUNT@2.0.0          <- COLLAB.INVITATION@3.1.0  an accepted invitation must bind to an authe…
  + ORG.MEMBERSHIP@1.2.0            <- COLLAB.INVITATION@3.1.0  acceptance creates a membership record

OBLIGATIONS  58 total   5 proven   53 unproven
PRODUCT LEVEL 0   (min over 7 capabilities, worst deficit -4)

CAPABILITY                     VERIF  SPEC  TGT         T1      T2      T3      T4      T5
AUDIT.EVENTS                      T0    T5   T1        1/3       -       -     0/1     0/2
BILLING.SEAT_ACCOUNTING           T0    T5   T1        0/2       -     0/1     0/2     0/1
COLLAB.INVITATION                 T0    T5   T3        1/6     1/3     0/6     1/2     0/3
EMAIL.DELIVERY                    T0    T5   T3        0/2     0/1     0/3     0/2     0/2
IDENTITY.ACCOUNT                  T0    T5   T4        0/2       -     0/1     0/1     0/1
ORG.MEMBERSHIP                    T0    T5   T1        1/3       -     0/1     0/2     0/2
SCENARIOS                         T0    T1   T1        0/3       -       -       -       -

VERIF is capped at SPEC: rungs the catalog never specified are not achievements.

SCENARIOS  0 of 3 business paths traversable end to end
  [ ] SCENARIO.REMOVE_MEMBER            UNPROVEN      An owner removes a member and that person immediately s…
        . an owner opens the member list
        . the owner removes a member
        . the removed person attempts an organization-scoped operation and is denied
        . the removal appears in the audit log with actor and target
  [ ] SCENARIO.INVITE_TO_MEMBERSHIP     UNPROVEN      A person named by an organization owner ends up able to…
        . an owner creates an organization
        . the owner invites a person by email address
        . the invitation message is accepted by the mail provider
        . the recipient opens the acceptance link and authenticates
        . a membership is created for that identity
        . the new member is listed and can act in the organization
  [ ] SCENARIO.RECOVER_ACCESS           UNPROVEN      A person who has lost their credentials regains access …
        . a person requests recovery for an address that has an account
        . the recovery message is accepted by the mail provider
        . the person opens the recovery link
        . the person sets a new credential
        . the person authenticates with the new credential
        . existing sessions issued before the change no longer authenticate

SKELETON   tier 1 and hoisted, exclusive priority  18 obligations
  [ ] a3bb0264  AUDIT.EVENTS             ISO.001     T4>1 crit For every actor A and tenant T where A is not …
  [ ] 4186f859  BILLING.SEAT_ACCOUNTING  ISO.001     T4>1 crit For every actor A and tenant T where A is not …
  [ ] 74e078cd  COLLAB.INVITATION        ISO.001     T4>1 crit For every actor A and tenant T where A is not …
  [ ] f116fed0  COLLAB.INVITATION        RACE.020    T4>1 crit Concurrent acceptance of the same invitation y…
  [ ] 0520e942  EMAIL.DELIVERY           ISO.001     T4>1 crit For every actor A and tenant T where A is not …
  [ ] 8eed6951  ORG.MEMBERSHIP           ISO.001     T4>1 crit For every actor A and tenant T where A is not …
  [ ] 4eed2e7c  SCENARIOS                TRAVERSE    T1   crit An owner removes a member and that person imme…
  [ ] 6886337b  SCENARIOS                TRAVERSE    T1   crit A person named by an organization owner ends u…
  [ ] cd32f26a  SCENARIOS                TRAVERSE    T1   crit A person who has lost their credentials regain…
  [ ] 80a5f858  AUDIT.EVENTS             EMIT.001    T1        An audit event can be emitted and later read b…
  [ ] 4e1853e3  BILLING.SEAT_ACCOUNTING  COUNT.001   T1        An organization's seats purchased and seats us…
  [ ] 032f4ed3  COLLAB.INVITATION        ACCEPT.001  T1        A recipient following a valid acceptance link …
  [ ] 2af84dfe  COLLAB.INVITATION        REVOKE.001  T1        An authorized member can revoke a pending invi…
  [ ] 46db9b6e  COLLAB.INVITATION        SEND.001    T1        An authorized inviter can create an invitation…
  [ ] 34aa9b82  EMAIL.DELIVERY           SEND.001    T1        A requested transactional message reaches the …
  [ ] 2c8c43c0  IDENTITY.ACCOUNT         AUTH.001    T1        A person can authenticate and receive a sessio…
  [ ] c07b718f  IDENTITY.ACCOUNT         RECOVER.001 T1        A person who has lost access can recover their…
  [ ] 75b5f429  ORG.MEMBERSHIP           REMOVE.001  T1        An authorized member can remove a membership, …

FLOOR      tier <= 1, schedulable  0 obligations
  (none)

NEXT       tier 2, schedulable only once the floor is met  3 obligations
  [ ] 421dea72  COLLAB.INVITATION        SEND.003    T2   crit An inviter may only assign a role at or below …
  [ ] 549d6926  COLLAB.INVITATION        SEND.004    T2        A created invitation expires 72 hours after it…
  [ ] 2c6bc004  EMAIL.DELIVERY           SEND.002    T2        Message status transitions from queued to sent…

ABOVE      tier > 2, not schedulable  32 obligations   polishing here is prohibited by the scheduler
  [ ] 046f6ff1  IDENTITY.ACCOUNT         RECOVER.010 T3   crit A recovery token is single use and expires, an…
  [ ] 096f2280  EMAIL.DELIVERY           OBS.030     T5        Delivery failure rate and queue depth are obse…
  [ ] 143f23ee  AUDIT.EVENTS             RETAIN.030  T5        Audit events are retained for the configured w…
  [ ] 1f57989b  IDENTITY.ACCOUNT         DELETE.030  T5        An account can be deleted, after which its per…
  [ ] 25b95194  COLLAB.INVITATION        ISO.003     T5        Cross-tenant access attempts against invitatio…
  ... 27 more (--all to expand)

WARNINGS
  ~ 3 behavioral obligations are supported only by static evidence (strength: fallback). A generated surface satisfies the shape of a behavior it does not implement. See generation-stack.md section 2.

Recorded output from fixtures/example-saas, the fixture the engine ships with.

Targets. In the capability table, TGT is the rung each capability must reach and VERIF the rung it has reached, capped at SPEC, the deepest rung the catalog populated for it. A rung the catalog never specified is not an achievement, and a capability targeted deeper than its entry goes is an authoring gap that blocks completion.

Unaddressed. Every one of the 53 unproven obligations has a binding or a test convention that says where to look, so each is a real absence of proof. When a profile cannot reach an obligation, the plan lists it separately so an absence of evidence is not mistaken for a failure.

Claimed and fallback strength. The warnings at the end name proofs the engine will not count at full strength: a behavioral claim supported only by static evidence, or a negative control the worker reported and the harness has not watched fail. They count toward done on their own advisory line and never toward a release.

The task envelope

next hands out the first obligation the scheduler allows, in the fixture’s case a hoisted tenant-isolation invariant on audit events. The homepage omits its sibling identifiers and the obstruction report format; this is the whole envelope.

TASK ENVELOPE  a3bb0264

obligation   POLICY.TENANT_ISOLATION.ISO.001   tier 4 (hoisted to the skeleton)   CRITICAL
siblings     4 other obligations share this catalog statement, one per resource:
             0520e942 (outbound_message), 4186f859 (seat_allocation), 74e078cd (invitation), 8eed6951 (membership)
             They are separate obligations with separate evidence. Proving this one
             proves this one. If your work genuinely covers the others, say so and the
             engine will record that judgment as a binding rationale rather than assume it.
capability   AUDIT.EVENTS
claim        behavioral
status       UNPROVEN

REQUIREMENT
  For every actor A and tenant T where A is not a member of T, no operation performed by A returns or mutates any audit_event owned by T.

WHY YOU OWE THIS
  <- POLICY.TENANT_ISOLATION@2.0.0  selector matched resource audit_event of AUDIT.EVENTS

PROOF THAT WILL BE ACCEPTED
  evidence kind   test.property (primary), test.example (fallback)
  negative control REQUIRED. This obligation is critical, so a passing
    test is not admissible on its own. You must also show the test FAILS when the
    implementation is perturbed. Suggested perturbation: drop.authz
    Record which perturbation you used and that the test failed under it.
  name the test  so that it contains the literal string [a3bb0264]
                 (that is how a passing test binds back to this obligation)

HOW IT WILL BE GRADED
  1. closure test --repo .
  2. the report at .closure/test-report.json is read for a passing test matching [a3bb0264]
  3. the files that test depends on are hashed; the proof expires when they change
  Nothing else counts. The grader is deterministic and this is its whole rubric.

AUTHORITY
  You may change   implementation, tests, migrations, configuration in fixtures/example-saas
  You may not      change this obligation, its catalog entry, its bindings, its tier,
                   or the evidence kinds it accepts. If you cannot satisfy it as
                   written, that is a report to file, not a requirement to soften.

IF YOU ARE BLOCKED
  Emit an obstruction report and stop. It must name this obligation, cite at least one
  machine-checkable observation with a file locator, and state the missing capability
  as an architectural class (durable_job_queue), never a product (kafka).

  {"kind":"obstruction","blocked_obligation":"a3bb0264afe5f208592662b412310bafe306aaea4f6fa2d83914a383e9dd3cc4",
   "claim":"<what cannot be satisfied>",
   "observed":[{"kind":"static.ast","locator":"src/x.ts:41","finding":"<what you saw>"}],
   "argument":"<why the observation blocks the requirement>",
   "missing_capability_class":"<lower_snake_class>"}

  Validate it with: closure obstruction <file>

The authority section is the part to read twice. The worker may change implementation, tests, migrations and configuration. It may not change the obligation, its catalog entry, its bindings, its tier or the evidence kinds it accepts, and an obligation it cannot satisfy as written is a report to file, not a requirement to soften.

The verdict

done prints every clause with the count blocking it. Two counts on this page differ on purpose. The plan reports 53 unproven obligations across the whole selection; the verdict reports 32, the ones required at the declared targets. The other 21 sit above target and are the next rung, not a debt.

DONE(example-saas)  =  FALSE

  + something is owed
      58 obligations selected
  x [32] every obligation required at the declared targets is proven
      32 unproven, of which 0 inadmissible and 2 stale
  + no obligation rests on unverified evidence
      supporting input digests were checked; control strength is reported separately
  x [7] every capability reaches its target level
      AUDIT.EVENTS T0/T1, BILLING.SEAT_ACCOUNTING T0/T1, COLLAB.INVITATION T0/T3, EMAIL.DELIVERY T0/T3, IDENTITY.ACCOUNT T0/T4, ORG.MEMBERSHIP T0/T1, SCENARIOS T0/T1
  x [3] every required scenario traverses end to end
      0 of 3 traversable
  + no capability is targeted deeper than the catalog specifies
      catalog is deep enough for every target
  + no unresolved gap objects
      closure reached a fixpoint with no conflicts
  + no contested obligations
      0 open
  + no blocking provisional obligations
      0 open
  + no pending weakening or exclusion requests
      these are the only changes a human must approve; everything else the engine derives
  ~ [3] advisory: proofs at full strength
      3 proven at fallback strength (weaker kind, partial surface, or self-attested control)

Blocked on: every obligation required at the declared targets is proven
This verdict is a property of the repository at this commit, not of this run.

The loop, as an authored model

The fixture stops at its first verdict. To show what the loop looks like after that, this interactive report carries an authored five-requirement example through three revisions: missing proof, a change that makes a proof stale, and a verified result. It is illustrative data, not the fixture’s output, and it does not read a repository.

Invitation acceptance

Interactive example

5Required

3Proven

2Remaining

Expired links are rejectedNo evidence

The behavior is required, but no admissible proof establishes that an expired invitation is refused.

Next task

Establish proof that expired invitations are refused.

DONE = FALSE2 requirements still need proof

Authored example data, not a live repository scan.

Would the test catch the failure?

The envelope above demands a negative control. This is what one looks like: the same test, run with the protection intact and then with only the expiry check disabled, in an isolated copy.

Expiry check Illustrative negative control

Same test, both runs“Expired links are rejected”

Protection intactTest passes

if (invitation.expiresAt < now) {
  return reject("INVITE_EXPIRED");
}

Expired invitation rejected

Disable only the expiry check

Protection removedTest fails

if (false) {
  return reject("INVITE_EXPIRED");
}

Expired invitation accepted

This test notices when the expiry check disappears.

This establishes sensitivity to the chosen perturbation, not proof of every possible failure.

Proof belongs to a code state

A proof records a digest of what it depended on. When the code covered by the expiry proof changes, the verdict moves on its own; the authored example below shows the transition.

Proof belongs to a code stateSame scope. Changed inputs. Different verdict.

DONE = TRUE5 of 5 proven
- Accept
- Expiry
- Revoke
- Replay
- Boundary
All requirements proven in this example’s scope.
The code covered by the expiry proof changes.
DONE = FALSE4 of 5 proven
- Accept
- Expiry
- Revoke
- Replay
- Boundary
Expiry evidence is stale. One requirement reopens.

Next taskRe-run expiry verification against the changed inputs.

Read the science

Why a green suite stops meaning done, what the mechanisms above rest on, and which of Closure’s claims are tested rather than argued.

The science behind Closure
Back to the recorded examples