open-standards/joulespec

JouleSpec — Energy-Accounted Specification Conformance

Version: 0.2.0-draft.1 · Status: Draft · Profile: joulespec/1 Specification text: CC-BY-4.0 · Reference code (joulespec-rs/): Apache-2.0

JouleSpec is the open standard for stating what software owes and measuring whether anything established it. A clause is addressed by its obligation, so renaming is free and rewording costs exactly that clause's evidence. Evidence climbs a ladder from testimony to proof. A revision yields the exact set of obligations that just lost their evidence. And the receipt says what the whole exercise cost in joules.

JouleSpec is one of the Transaction Science open standards.

The problem is measurement, not methodology

Specification-driven practice converged on a shared shape: write the intent down, derive the plan and the implementation from it, review at each phase. The artifact it produces is prose an agent interprets and a human reads, and the difficulties that follow are catalogued consistently wherever the practice is examined — specifications drifting from the code they describe, generated artifacts trusted past their evidence, no method for checking that an implementation conforms, and a review burden heavy enough that practitioners report preferring to read the code.

Each of those is a measurement problem wearing a methodology costume, and each persists for the same reason: the specification is a document. A clause cannot be addressed, so nothing can bind to it. Conformance is a sentence in a review, so it cannot be graded or capped. The cost of the ceremony is an anecdote, so the argument about whether it is worth the effort has no units and cannot be settled.

JouleSpec changes none of the methodology. It changes what the specification is.

Renaming is free; rewording is not

A clause carries a label and an obligation. The label — C1, auth-2 — is editorial. The obligation is the content address of the clause's kind and text, with the label deliberately excluded (SPEC §1.2), and evidence binds to the obligation.

  C1  "The endpoint rejects unauthenticated requests."    → b3:9f4c…
  auth-2  "The endpoint rejects unauthenticated requests." → b3:9f4c…   same obligation
  C1  "The endpoint should reject unauthenticated requests." → b3:2e71…  different obligation

Renumbering a whole specification moves nothing and loses no evidence. Weakening one requirement by one word invalidates that clause's evidence and nothing else's — automatically, with nobody having to notice.

Binding evidence to a label gets both halves backwards: it survives the edit that changed the requirement and breaks on the edit that renamed it. That inversion is the mechanism by which drift goes unobserved. It is an addressing problem, not a discipline problem, and an address is the whole fix.

A ladder ordered by one question

How hard would it be for this obligation to be violated without this evidence noticing?

E0	cited	The implementer says it is done. Nothing noticed anything.
E1	reviewed	A second party read the artifact, once.
E2	exercised	A named check ran against the artifact and passed.
E3	falsifiable	The same check is on record failing against a named counter-artifact.
E4	proved	No input violates it, under a formalization someone independent checked, shown not to hold vacuously.

Every rung above E2 rests on a demonstrated failure, and the rule binds proofs as much as tests. A formal property can be satisfied vacuously — true because nothing ever reaches the condition it guards, so it would hold of almost any implementation; detecting that is established practice in model checking, and one industrial setting reported around a fifth of specifications initially passing that way. So E4 requires the statement to have been refuted against a named counter-model, exactly as E3 requires a check to have failed against a counter-artifact.

E0 is where prevailing practice lands, and it is testimony from the party being evaluated. Much of it is true; it is still testimony, and reporting it as conformance is the error this standard exists to stop.

E2 flatters. A green check establishes that something ran. A test with no assertion passes, and so does one whose fixture never reaches the condition the clause cares about.

E3 is the first rung where green means something — the check has demonstrated it can fail, so its passing carries information. It is also the cheapest strong rung: most projects can reach it with tests they already have, by recording the mutant the test was written against.

The ladder is ordered by re-checkability, not diligence. A review is bound to the state a person looked at; a named check runs again against any later state. That says nothing about how carefully anyone read the code — it says one kind of evidence survives the next commit and the other does not.

Independence is computed, never declared. A review signed by the key that made the citation is the citation again, and grades E0 (SPEC §2.5).

Where the expectation comes from

Whether a check can fail is not only an empirical question. An oracle whose expected value is derived from the system it judges cannot disagree with that system when a fault moves the measurement and the expectation together — the comparison cancels, and no input reveals the fault. The defect is in the oracle, not the inputs, and it is visible from the oracle's construction without running anything.

So every check declares an anchor: specification (expected values fixed outside the code under test — the spec, a published procedure, a reference table), state (values flowing from the code under test), or unstated. An unstated anchor caps a check at E2, because whether an oracle reads its expectation from its own subject is knowable to whoever wrote it at no cost, and silence is not an answer. A state-anchored check that killed a mutant did fail once and reaches E3 — with its anchor disclosed, because the class of faults it cannot catch is disclosed with it (SPEC §2.5).

Evidence that survives a change it did not depend on

Binding evidence to a whole-tree digest alone would make every commit stale every witness. That is the documented way traceability dies: the empirical literature finds trace links degrade mainly through ordinary refactoring, and reports that keeping them current can cost more than creating them. A standard whose evidence expires on every unrelated edit has reproduced that failure however sound its addressing.

A witness therefore names a footprint — the addresses within the artifact it actually depended on — and applies at any later state whose parts still contain every member (SPEC §2.4). Edit the documentation and the evidence for the auth requirement stands; edit the auth code and that clause ages, alone. Paths never enter the mechanism: a content address is the identity of its content.

A footprint is a producer's claim that nothing else mattered, signed with the rest of the witness, and a narrower one is a stronger claim — so a wrong footprint makes the evidence wrong rather than merely stale. An empty footprint means the whole artifact, which is what a producer that cannot enumerate its inputs must use.

Two axes, because they fail separately

How strong a check is and how independent the party reporting it is are different questions. Collapsing them loses the one that matters most where the implementer and the reporter are the same process — the normal case for an agent that writes code and then reports that it works.

A0	self-attested	The party reporting the result did the work.
A1	independent	Signed by a key that authored none of the work.
A2	reproduced	Two disjoint parties reported the same check at the same grade and state, at least one independent of the work.

Both axes gate conformance (SPEC §3.4). Attestation is derived from work authorship and from agreement between disjoint keys — never declared — and where no work was supplied it is absent rather than independent: absence of information about who built something is not evidence that someone else checked it.

What an E4 actually claims

A proof discharges a formal statement, and the statement is not the clause. The binding between them is a human act and the weakest link in any claim of proved conformance — so a proof reaches E4 only when that binding was cross-checked by a key other than the prover's. Under a merely declared formalization it grades E2: real mechanical evidence about something, where that the something is this clause remains the prover's word (SPEC §2.6).

The reference library never formalizes a clause on anyone's behalf. Demotion rather than refusal is deliberate — the proof is not fake, and discarding it would lose evidence that exists.

The weakest obligation sets the grade

A specification's grade is the minimum over its requirements and constraints, absent entirely when any of them has no surviving evidence (SPEC §3.2). Averaging would let nine proved obligations conceal one nobody looked at, which is the failure a grade exists to surface.

Non-goals are first-class and handled differently. There is nothing to evidence about behaviour that should not exist, so an unwitnessed non-goal is correct and carries no grade. Evidence that one was implemented is a flag: it does not lower the grade of the owed obligations — they really are evidenced — and it does block conformance. The specification said not to build this and something says it exists.

Nothing is dropped quietly. A witness that does not verify, names another specification, or names an obligation the specification does not state is a reported finding, not a no-op. That last case is the normal aftermath of a rewording and the clearest available signal that evidence and specification have parted company.

Drift is a partition, not a warning

Diffing two revisions by obligation address says exactly which evidence survives (SPEC §4.1): obligations kept, relabelled (editorial — no evidence lost), reworded (that clause's evidence invalidated, the new obligation unevidenced), added, and removed. From those, the two sets a revision review actually wants fall out: what just lost its evidence, and what starts unevidenced.

A freed label reused by a new clause is an addition, not a rewording — the old obligation still stands elsewhere, so no evidence is invalidated, and conflating the two would report a loss that did not happen.

The other direction of drift is the artifact moving under evidence that stayed still, and it needs no diff at all: a witness is bound to the artifact state it observed, so evidence from an earlier state is reported stale rather than counted (SPEC §3.1). Neither direction requires anyone to remember to check.

The ceremony has a price

Every witness carries the energy it cost to produce, and every unit of work carries the energy it cost to perform. From that the receipt seals two figures nothing else in this space can state:

• The specified share — how much of the work energy went into work citing an obligation this specification actually states, in parts-per-million (SPEC §5.2), with the work that cites nothing named rather than only counted. Certified-airborne-software practice has required traceability in both directions for decades, and the backward direction exists for one purpose: code with no upstream requirement is a finding even when it works correctly, because unintended function is what the argument cannot otherwise exclude. A figure answers how much; only the list answers which.
• Microjoules per falsifiable obligation — total attributed energy over the count of owed obligations evidenced at E3 or better (SPEC §5.3). The denominator is deliberately the rung whose evidence can fail: a figure per attempted obligation rewards ceremony, a figure per obligation something would have caught rewards evidence.

Whether specification-driven practice earns its overhead is currently settled by anecdote in both directions. Two processes applied to the same specification, reaching the same evidence, one spending an order of magnitude more energy to get there — that is not a matter of taste.

Where nothing reaches the bar the figure is absent, not zero. A cost per unit of nothing is not a small number.

And it is comparable only at a fixed specification address (SPEC §5.3). Any figure of the form things evidenced over things total improves when you add trivial things — the standing objection to counting resolved doubts in assurance argumentation — so splitting one requirement into twenty trivially falsifiable ones would divide this figure by twenty while establishing nothing. The receipt seals the specification's address precisely so a reader can tell whether two figures are comparable at all. The grade and the attestation carry no such caveat: both are minima, and a minimum cannot be improved by adding obligations.

The receipt is derived, never signed on request

A receipt is sealed from the specification, the artifact, the witnesses and the work — never from a verdict handed in (SPEC §6.1). A verdict is an ordinary data structure, and an interface that signed one would let a producer construct the grade it wanted. Because the receipt is derived from the evidence, every claim in it is reproducible by anyone holding the same inputs, and a producer who wants a better grade has to go and get better evidence.

Receipts seal as joulespec/1 JCR-1 envelopes — canonical det-CBOR under COSE_Sign1 with Ed25519, the wire format the rest of this family seals with, so a receipt verifies under tooling that has never heard of JouleSpec. The core admits no nulls and several figures are legitimately absent, so those fields are omitted rather than zeroed: a reader who finds no grade knows none was established, where a reader who found E0 would believe one was.

Each receipt carries a per-clause audit — label, kind, obligation, grade, the witness that carried it, evidence energy, stale count — because which obligation is the weak one is the actionable fact, and it must be answerable from the receipt alone (SPEC §6.3).

Relation to existing work

Structured assurance cases already standardize the shape of the argument — claims decomposed to sub-claims until each links to evidence — and the international standard for their structure is explicit that it does not set quality requirements for the content. The grade of a piece of evidence is exactly that content question, so joulespec/1 adopts the vocabulary and supplies the part left open. Certified-airborne-software practice supplies the bidirectional rule, and grades structural coverage on a ladder of its own that composes with this one rather than competing: coverage says how thoroughly a check exercises the code, an anchor and a killed mutant say whether it can fail at all. Supply-chain provenance frameworks grade the build record and say nothing about correctness — that is the A axis, not duplicated here. Carbon-intensity accounting for software is an international standard shaped as a rate per functional unit of work, which is the shape of §5.3, and it covers the energy of running software where this covers the energy of producing it. Full treatment in SPEC §9.

What it does not do

JouleSpec does not write specifications, run checks, formalize clauses, or judge whether a clause states a good requirement.

And it cannot tell whether a clause says what its author meant. An obligation is addressed, signed and tracked, and may still be the wrong requirement. Software can satisfy every clause of its specification and be unfit for purpose, because the specification was incomplete — and an incomplete specification is exactly the case where every clause is covered. A grade is a property of evidence, not of software (SPEC §8).

Three limits are worth stating here because they bound what the mechanisms above can establish. A footprint is trusted, not verified — a producer that narrows a witness to inputs its check did not read gets evidence outliving the change that invalidated it; the claim is signed and attributable, and this standard cannot tell what a check actually read. A2 is agreement, not correctness: reproducing a vacuous check reproduces the vacuity. And two of the results this design builds on are thinly evidenced — the vacuity rate comes from one industrial setting and the oracle-anchoring effect from a single-system study — so the design rests on the mechanisms, which stand on their own, rather than on the magnitudes.

Reference

joulespec-rs/crates/joulespec-core — obligation-addressed clauses and signed revisions (spec), the graded evidence ladder with anchoring, vacuity and computed independence (evidence), the deterministic two-axis evaluator with the weakest-obligation cap and footprint-aware staleness (conform), the revision partition (drift), and the joulespec/1 JCR-1 receipt derived from its inputs (receipt).

Prior art inside this family: joule-code-spec first shipped the signed, content-addressed clause and the citation binding a coding operation to it. Its citations bind by clause label and its audit has one notion of coverage — a clause is covered when something claims it. That is the E0 rung here, and label binding is the drift hole this standard closes.