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).

The producer, and the standard applied to itself

A schema nobody can emit into is a schema. joulespec-cli is the reference producer: it reads the clauses from a published specification document, runs each declared check, runs it again against a counter-artifact, and emits a signed witness at the rung the observations support.

joulespec harvest --manifest conformance/v1/harvest.toml \
                  --out conformance/v1 --require-grade E3

It refuses to confuse the three ways a run can fail to pass. A test that did not run is not a test that passed — a harness filtered to a name nothing matches prints running 0 tests, reports success and exits zero, so the count is checked. A counter-artifact that did not compile demonstrates nothing, because the check never ran; treating that as E3 evidence would manufacture falsifiability out of a syntax error. And a counter-artifact that compiled, ran and passed is a finding: the check cannot see the thing it is about. The harvester exits non-zero on findings, so a pipeline can gate on them, and CI gates on this one.

It reads someone else's specification, not only this one. Requirements live in a few conventional shapes — a numbered conformance list, a bulleted requirement list, a heading per requirement carrying its identifier — and which one a document uses is a fact about that document, so the manifest declares it:

[spec]
document = "docs/requirements.md"
section  = "2. Requirements"
shape    = "heading-label"     # or bulleted-bold-label; omitted = numbered
expect_at_least = 14           # the floor still fails closed

Run against this family's other specifications — documents written without this producer in mind — the bulleted shape reads their conformance lists and the heading shape reads a normative companion kept as one section per obligation. What does not read is reported rather than returned empty: a conformance section written as a table of profiles, or as numbered prose with no labels, says it holds no items of the declared shape. joulespec clauses exists for exactly this, because the alternative is discovering a mis-declared shape through an item count, which says nothing about which items were missed.

Doing that found two things. In the producer: a bullet carrying a bold label the splitter could not read was being folded into the item above, which appended a different item's words to that obligation's addressed text — a soundness bug, since the obligation then says something nobody wrote. It now fails closed, and a bare label like **C-neg:** reads as the item it is. In a sibling standard: its conformance section enumerates a clause its own normative companion never defines, so that obligation could never have been evidenced by anything.

Nothing else about the extraction varies, and a heading that states no requirement is not read as one — addressing the empty string would create an obligation nobody wrote and then grade it. Changing the declared shape moves every obligation address, which is correct rather than unfortunate: a different extraction describes different obligations. It does mean the shape is part of what an auditor needs in order to recompute them.

Three things in the manifest are declared because they are human judgements the standard refuses to guess: which check stands for which obligation (the same act as formalizing a clause, SPEC §2.6), each check's anchor, and each check's footprint — a harness that cannot observe its own reads must not guess (SPEC §8). Everything else is computed.

The standard is applied to its own implementation. Every conformance item of SPEC §7 is mapped to a check with a counter-artifact, and the clauses are read from the published SPEC.md rather than copied into the manifest, so the manifest cannot drift from the specification: reword an item and its obligation address moves, invalidating the evidence bound to the old wording.

Doing that found two things inspection had not. A footprint test narrowed to a single member, and on a one-element footprint all and any are the same function — so mutating the conjunction left the test green, and the conjunction was never actually checked. And a guard in applies_at could not change a single verdict: an all over a non-empty footprint against no enumerable parts is already false. The guard looked like care.

Extending the standard found a third. Pulling two rules out into named functions — so a prover could be asked about them over their whole input domain — moved the text two existing counter-artifacts were aimed at, by a single indentation level in one case, and both silently stopped describing any edit at all. The harvester refused to run, which was right but late, so it now validates every anchor before running anything. Tolerating a missing anchor would have been the real failure: two clauses would have gone on looking falsifiably evidenced while nothing was being mutated.

All of it is recorded in conformance/v1/README.md, and that is the E3 rung doing the only thing it claims to do.

Applied to a standard that is not this one

A producer that has only ever measured its own specification has demonstrated a format, not a method. proof/conformance/v1/joulespec.toml points this producer at a sibling standard: its conformance items are read from that standard's own published document, each is mapped to a named check in its workspace, and each mapping declares a counter-artifact that must make that check fail. Every item of that standard's conformance section reaches E3, and CI gates it there under applied: — so a refactor that moves the code a mutation was aimed at makes the harvest refuse, and a check that stops being able to fail becomes a finding instead of staying green.

Doing it found one thing, and the shape of the finding matters more than the finding. The first counter-artifact for that standard's routing clause was aimed at a constant the router turned out not to read, so the check passed with the constant reordered and the harvester reported that the check could not see its subject. The report was right; the manifest was wrong. A producer can say only what it observed — that a check passed while something it was supposed to notice was broken — and whether that means the check is weak or the mutation missed is the operator's call. Re-aimed at the sort that actually orders the rungs, the same check failed at once, which is how the clause's evidence ended up real rather than assumed.

Conformance packs

Three, answering different questions:

• conformance/v1/vectors/ — the certifiable surface. Fixed keys, clauses, witnesses and energy, byte-stable, carrying one witness of every rung plus one bound to a superseded state so an implementation that mishandles staleness fails rather than passes quietly. Its verdict is the doctrine in miniature: two obligations well evidenced, one carrying only the implementer's citation, and the specification therefore graded E0 at A0.
• conformance/v1/evaluation/ — the verdicts, not the bytes. Round-tripping a receipt says nothing about whether an implementation graded correctly, because the vectors carry one scenario. Each case here is a complete set of evaluation inputs plus the verdict §3 requires, chosen so that a plausible but generous implementation disagrees: a mean where a minimum is required, E3 awarded on a killed counter-artifact whose anchor is unstated, E4 awarded because a prover succeeded, a witness for a clause's previous wording discarded instead of flagged. Most cases catch over-grading; at least one catches under-grading, because an implementation that graded nothing would pass all the others.
• The self-conformance receipt beside them — a measurement, not a vector. Its energy comes from a wall clock, so re-running the harvest produces different bytes. A pack that held measured energy fixed would be publishing a figure nobody measured.

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).

joulespec-rs/crates/joulespec-cli — the reference producer: clauses parsed from a published document (specdoc), the artifact state and its part addresses (tree), the declared mappings (manifest), the check runner with its three-way distinction between a run that failed, one that did not compile and one that should not have passed (runner), and the harvest itself (harvest).

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.