How it works
It reads your contract, not your test file.
A contract states more than the shape of a call. Which field carries an entity’s identity, how entities correlate, which states a thing can occupy, which principal may invoke what. Tools that read your specification stop at the message shape and leave the rest of the document where it was.
The truth, the loss, and the recovery
Your contract already contains a verification model. Not a sketch of one. The operations, the entities, the identities, the lifecycles and the permissions are all stated in it, by you, in a document you already maintain and already ship.
That model gets re-typed by hand into a test suite, where nothing can check it against the document it came from. From that moment the two drift, and the suite’s greenness stops being evidence about the system and becomes evidence about the transcription.
Derive the model instead of transcribing it. Recompute it on every compilation so it cannot fall behind. Then a scenario can be checked against your contract before it runs, and coverage has something to be a fraction of.
What a derived surface is
The maximal set of facts establishable from the contract alone: every operation with its field shapes, every entity, which field carries an entity’s identity, how entities correlate, which states a thing can occupy, and which operations are observable.
And, which is half the definition, what it will not conclude. Anything the contract does not state stays unstated. An identity that cannot be read back is reported as exactly that, with the operation and field named, rather than guessed at.
It is recomputed on every compilation, so it cannot fall behind the contract.
analyze also writes an assumptions.yaml beside your project:
it records what was derived, and it is where you state the few things a contract leaves
unsaid. SODL keeps its own lines in it current, and most projects never open it.
schema Order: identity `order_id`
schema Shipment: identity inferred from path parameter
schema Adjustment: no identity property found;
cannot treat as a resource
WARNING Refund [IdentityNotObservable] — identity "refundId"
is a request parameter of getRefund but not a field of the
response shape — no join was written, so this entity cannot
be observed by identityThree outcomes and a refusal. The refusal is the interesting one: it names the operation and the field rather than inventing a join.
The compile gate
Every name in a scenario is resolved against the surface before anything runs: the operations, the fields, the actors, the states. A scenario that no longer fits the contract does not run and pass against a system that has moved. It is refused, with a position. This is the difference between a test that goes red because an assertion failed and a test that never got the chance to lie to you.
$ sodl check
Checking contracts & derivation... ✓ PASS contracts resolved; semantics derived cleanly
Running scenarios... ✗ FAIL 0 passed, 0 failed, 1 uncompilable
Checking coverage... ✓ 176 of 341 operations exercised; all 14 resources observable or readable
────────────────────────
Verification: failed
Findings
✓ Contracts & derivation: contracts resolved; semantics derived cleanly
✗ Execution: 0 passed, 0 failed, 1 uncompilable
✗ scenarios/orders/approve.sodl:12:18: SHIPPED is not a state of OrderStatus
✓ Coverage: 176 of 341 operations exercised; all 14 resources observable or readable
ℹ 165 operations unexercised — `sodl coverage` lists themSomeone renamed a state in the contract. The scenario stopped compiling in the same commit, rather than going green against a service that no longer has that state. Note the middle line: nothing ran, so nothing passed, and the verdict says so instead of reporting a clean sweep of the scenarios that still compiled.
The denominator
A fraction needs one. Denominators exist today: lines in a file, branches in a function, operations listed in a document. Each measures something real. But a line-coverage denominator counts your own test code rather than what your service can do, and an operation count stops at the operation.
Because the surface was derived, there is a denominator over all of it, down to the states a thing can be in and never reaches.
$ sodl coverage Operations: 176 of 341 exercised Orders: 92 of 121 exercised Invoices: 54 of 118 exercised Shipments: 30 of 102 exercised Negative paths (fails asserted): Orders.GetOrder, Invoices.GetInvoice Entities: 11 of 14 asserted-on, 3 untouched Order: bound, asserted-on Invoice: bound, asserted-on Refund: untouched Adjustment: untouched Dispute: untouched Lifecycles: Order.status (OrderStatus): 2 of 4 states asserted (PENDING, APPROVED) Invoice.state (InvoiceState): 0 of 3 states asserted
Excerpt: nine of the fourteen entities and the per-operation breakdown are cut. Disclosure, never a gate. No threshold, no score, no effect on any exit code.
Drift
Contracts change; that is what a living system does. The failure is that a change gets noticed by whatever happens to exercise it. A removed field nothing covers passes every gate, and the suite is green because the change was invisible to it, not because it was safe.
Tools that diff contracts exist and detect breaking changes at the document level. That is not a capability SODL introduced. What a diff answers is did the document change? Drift answers a different question: did it change away from what was proved? The comparison is against the contract snapshot a release was verified against, bundled with the scenarios that verified it.
$ sodl drift release-bundle -against . Uncovered breaking changes (no scenario in the bundle exercises these): Invoice: entity removed (orders.proto:23) GetOrder.customer_id: field removed (orders.proto:19) Order.status: state APPROVED removed Counts: 0 broken, 0 pre-broken, 3 breaking changes, 0 informational changes
Zero broken and three breaking, which is the case worth showing: nothing in the bundle exercises any of them, so no scenario went red and the gate fails anyway. The state removal carries no source position, because its position in the baseline is not known. It is reported without one rather than with a guessed one.
What survives a run
One immutable record per run, written once and never reopened. What ran, against which contract by digest, in which environment, when, by which build, and with which identities. The report page is a rendering of that record and adds nothing to it.
The rule the record follows is that every observation consumed in a verdict appears in the record, or is discarded by a documented law. There is no third option where something influenced the result quietly.
"environment": {
"name": "staging",
"source": "environments/staging.yaml",
"endpoint": "orders.staging.internal:50051"
},
"sodl": {
"version": "0.1.0"
},
"startedAt": "2026-08-02T09:14:22Z",
"finishedAt": "2026-08-02T09:21:07Z",
"counts": {
"pass": 168,
"fail": 12,
"skipped": 18,
"notServed": 4,
"unsupported": 3,
"uncompilable": 9
},
An excerpt of .sodl/runs/20260802T091422Z.json, in the file’s own key
order and its own formatting. The keys either side of this, cut here, are the contracts
and their digest, the scenario tree, and the identity acquisitions: one of those failed,
which is why 18 scenarios never reached execution and are not counted as passing.
Six states, because three would be a lie
Most runners have two outcomes and a bucket called skipped. That bucket hides the difference between we chose not to, your deployment did not answer, and this tool cannot do that yet. Those are three different problems with three different owners, and collapsing them moves the work onto whoever reads the report next.
The scenario ran against the live system and every expectation held.
It ran and an expectation did not hold. Your system, or your scenario; the message and the position say which.
The scenario never reached execution. Usually an identity could not be acquired, or something it depended on did not happen.
A deployment fact, not a scenario fault. The operation is in the contract and the running service did not answer it.
A SODL v1 boundary, not a fault in your system. Ours, named as ours, and on the same page as the passes.
The scenario does not compile; nothing was verified. It says nothing about the system under test, which is why it is not a failure.
Those sentences are the product’s own. Each has exactly one home in the source and is printed from there, so the report, the console and this page cannot disagree.
The objection worth taking seriously
Derivation inherits the contract’s defects. If the contract is wrong, the model is wrong, and you prove the system matches a lie, with more ceremony than a test suite would have used.
True, and central. What SODL does about it is narrow and worth stating precisely. Constructs it cannot model become named representation gaps rather than guesses. Ambiguity is refused by name. Contract change is caught by drift. What it does not do is detect that a correctly written contract describes the wrong system. Nothing reading the document can do that, and a tool claiming otherwise would be the thing this one exists to argue against.
The argument at length, for a reader who wants it: why verification begins at the contract →