Verification for distributed systems

Don’t assume. Prove it.

Your suite is green. That is a fact about the tests someone wrote, not about the system you are shipping.

SODL reads your service’s own contract, derives what is actually verifiable from it, runs your scenarios against the live system, and writes down what it proved. Fresh, every run, and nothing test-related ever goes into your contract.

Get started in one minute How it works

gRPC / protobuf · OpenAPI 3.0 · Swagger 2.0 · free to use, no account, nothing to sign

scenario CreateAndApprove {
  customer = CreateCustomer( name: "Ann" ) as admin
  created  = CreateOrder( customer_id: customer.customer_id ) as customer
  expect created.order_id != ""
  order    = GetOrder( order_id: created.order_id )
  waitUntil order reached APPROVED
}

The vocabulary is your system’s, not a testing language’s. Every name in it is checked against your contract before the scenario is allowed to run: the operations, the fields, APPROVED.

Run this before you write any tests.

No running service. No credentials. No deployment. sodl analyze reads the contract you already ship and answers questions your suite structurally cannot.

Which entities can be created but never read back. Which state fields are plain strings, so no vocabulary can be enforced on them. Which operations your contract cannot tell apart. How much of the surface anything touches at all.

What it finds on a real contract →

$ sodl analyze

=== Verification Surface Summary ===

Resources
  Observable     : 12 / 14
  Potential reads: 2
  Blind spots    : 0

Lifecycles
  Total             : 6
  Contract-def      : 4  (enum)
  String-typed      : 2  (vocabulary unverifiable)
  Partial lifecycles: 2

=== Findings (23) ===

[PartialLifecycle]
  WARNING Shipment [PartialLifecycle] — state field `state` is
          `string`; vocabulary not contract-validatable

=== Scenario coverage ===

176 of 341 operations exercised

3 of 14 entities untouched
  untouched: Refund, Adjustment, Dispute

An excerpt: the findings list and the observation tables are longer. Line formats are SODL’s own; orders-api is the worked example carried through this page.

Three questions to put to your current suite

Which operations does no test touch?

Your test runner cannot: it knows the tests you wrote and nothing else. Counting the operations a document lists gets you partway. SODL derives the whole surface, so the denominator reaches past operations to the entities, the fields and the states nothing ever reaches.

Can it fail a deploy for a field that nothing tests?

Removed fields, removed operations and removed states break consumers whether or not you happened to cover them. SODL compares contracts, not just tests, so an uncovered breaking change still fails the gate.

Can you prove what verified, against what, last Tuesday?

Every run writes an immutable record: what ran, against which contract, in which environment, when, and by which build. A system of record, not a report that scrolls off the terminal.

One contract. One derived truth. Many verifications.

The surface is recomputed every time anything compiles, so it cannot drift from the contract. Coverage, the drift gate and the record are all consequences of that one act.

You own this

Your contract

A .proto or an OpenAPI document. Untouched. Nothing test-related ever goes into it.

derive

Recomputed every run

The verification surface

Operations and field shapes. Entities, and which field is identity. Lifecycles, and the states a thing can be in. Who may call what.

compile

You write these

Your scenarios

All of them checked against the one surface. A scenario that no longer fits is refused before it runs, not twenty minutes into a red build.

run

SODL writes this

The evidence

Executed against the live system, then written down once and never reopened.

The artifact

A page you can hand to someone who was not there

sodl report renders the run as one self-contained page. This is the top of it, which is the part that matters. Everything below is the detail behind these numbers.

The layout, the state names and their sentences are the report’s own; the colours are this site’s. orders-api is a worked example, and every number on it, the widths of the bar included, is computed from the others.

Where it fits, and where it does not

SODL earns its place where a workflow crosses services or takes time to settle. Where that is not the shape of your problem, an ordinary test framework is the right answer, and SODL will not pretend otherwise.

Read the limits in full →

Good fit

Workflows crossing several services
Asynchronous state that settles later
Contracts that change under you
Release gates that must be defensible

Not this

UI testing
Load and performance testing
Unit tests
Systems with no published contract

Point it at a repository you already have.

Not a demo project. The whole claim is that SODL derives a model from your contract, so a curated showcase is the one artifact that cannot demonstrate it.

No account, no token, no sign-up. Nothing on this list needs a running service, and the probe writes nothing at all.

Start Read the limits first

curl -fsSL https://github.com/rajsinghsisodia/sodl-releases/\
releases/latest/download/install.sh | sh

sodl init -probe    # read-only: prints what it found
sodl init -yes      # writes sodl.yaml and a starter scenario
sodl analyze        # still no service needed

Windows has a PowerShell one-liner. -probe exists because discovery walks a convention, and a repository that does not match it should say so before anything is written.

Contracts	4c1f9ab27de0 · 2 sources all 2 sources orders/api/orders.proto orders/api/invoices.proto
Environment	staging · 1 transport routing default grpc → orders.staging.internal:50051
Operations	176 / 341 exercised
When	2026-08-02T09:14:22Z · sodl 0.1.0