Machine-checkable software-engineering pipeline

01 / Define the contractFormal requirements

Start with a small ticket/card/whatever: what should change, for whom, and what must remain true. Give properties stable identifiers so the same requirement can be traced through the model, tests and production.

• Safety: something bad never happens. Example: a command ID causes at most one committed mutation.
• Liveness: something good eventually happens. Example: an accepted command eventually receives an outcome, provided the server recovers and communication resumes.
• Assumptions: the conditions under which the claims hold, including durability, eventual connectivity and scheduling fairness.
• Structural rules: domain code cannot import "X package" or "Y package" adapters, handlers delegate business operations to application services.

Use TLA+ for states, transitions and temporal properties. Keep product intent and structural constraints alongside it. Not every ticket needs a new model: routine UI changes can reference existing contracts.

What I say ticket/card/whatever I actually mean a set of files (this step is hard and should be taken seriously):

feature/
  requirements.md          Human intent + property IDs
  Feature.tla              Behavioral specification
  Feature.cfg              Model-checker configuration
  architecture-rules.*     Executable dependency constraints
  assumptions.md           Scope, failures and trust boundaries

02 / Explore resilienceArchitecture search

Use Residuality Theory, developed by Barry M. O'Reilly, as a way to challenge designs: expose a candidate architecture to stressors and examine the useful capabilities or structures that remain: the "residues". Compare candidates and document tradeoffs.

For example, for a WebSocket service, we could imagine some of the stressors being: duplicate commands after reconnect, database unavailability, a process crash after commit, delayed broadcasts, authorization revocation and traffic spikes. These must be random, do not use probability there, include combinations and failures outside the happy path. Check Residuality Theory to learn more about it.

A stressor/residue incidence matrix can organize the analysis. Its entries need defined meanings and evidence, a matrix calculated from guesses does not establish resilience.

03 / Verify the designFormal design verification

Refine the behavioral model to include the selected architecture. An outbox, retry queue or separate broadcaster introduces states and failure windows that the initial requirements model may not contain.

Model persistence, acknowledgement, retries, crashes, recovery and synchronization. Ask whether the properties survive every behavior covered by the chosen verification method.

Check that the model permits meaningful progress and that properties are not passing vacuously. A system that never acknowledges anything trivially satisfies “no ACK before commit.” Liveness needs explicit fairness and recovery assumptions.

A counterexample is a design review input. Fix the transitions or revise an incorrect assumption through review, do not relax the property merely to obtain a passing result.

04 / Build against the contractImplementation

The coding agent receives the approved specification, selected architecture, relevant source files and executable boundary rules. It implements the feature and maps important model actions to code paths.

Make constraints enforceable. For example, use dependency-cruiser, linter import restrictions or Nx module boundaries to prevent domain modules from depending on infrastructure. Typed languages and runtime schemas enforce complementary data contracts.

Instructions in AGENTS.md and ADRs provide context, CI rules enforce the parts that can be checked. Protect requirements, model properties, verification harnesses and release gates using permissions and independent review.

05 / Close the model-to-code gapModel-based conformance testing

A verified model does not verify the programming language implementation. This stage checks whether real executions correspond to behavior permitted by that model.

Build a harness that generates model actions, translates them into application operations, observes the result and compares abstract state. For example, Retry(cmd1) becomes a resend over a real connection, “processed once” becomes a query of committed effects in the test database.

• Model-based tests: generate operation sequences and compare them with a state-machine oracle.
• Property-based tests: vary payloads, commands and schedules, then shrink failures to a minimal reproducible case.
• Trace checking: map recorded events into model states and check legal transitions or named properties.

Define the abstraction carefully: internal implementation steps may correspond to stuttering in the model, and concurrent executions cannot always be compared using one naive total ordering. For objects that promise it, linearizability checking can compare concurrent histories with a sequential specification.

06 / Check the applicationConventional verification

Run the checks that catch implementation mistakes outside the abstract protocol: unit tests for business rules, integration tests for persistence and adapters, and E2E tests for actual user journeys.

Add type checking, runtime validation, dependency rules and relevant security analysis. Verify migrations and compatibility when the change affects stored data or older clients. Agents may write additional tests, but an independently reviewed oracle should define the expected result.

Loop implementation and tests until the checks pass. A changed expectation or deleted test is a contract change to review, not an ordinary fix.

07 / Challenge the executionAdversarial verification

Run the implementation under controlled faults: delayed database responses, disconnected clients, process termination, restart, resource pressure, malformed inputs and simultaneous retries.

For a more systematic approach, build deterministic simulation: replace clocks, scheduling, randomness and network delivery with controlled interfaces. Explore schedules and replay failing seeds. Real-service fault tests still matter because a simulator abstracts away deployment behavior.

Respect transport semantics. A live WebSocket over TCP provides ordered delivery on that connection. Model stale, duplicated or differently ordered application events where retries, reconnects, queues or multiple connections actually allow them, do not invent arbitrary frame reordering within one intact connection.

Evaluate the same properties used earlier, rather than merely checking that the process stayed alive. Bound recovery checks with a documented operational timeout, a finite timeout alone does not establish mathematical eventual progress.

08 / Release through an evidence gateControlled deployment

Ship only when the predefined checks for the feature's risk level pass. The gate verifies evidence attached to the exact release artifact, rather than accepting an agent's summary.

Use staged rollout or a canary where appropriate, define rollback triggers, and ensure recovery is compatible with data migrations. A rollback may require a forward fix or data repair, reverting a binary does not undo committed database changes.

Near-autonomous releases need narrow deployment permissions and a policy for when to stop. Requirements changes, destructive migrations or an unexplained failed invariant should route to human review according to that policy.

09 / Keep checking after releaseRuntime verification

Instrument the application with command IDs, commit outcomes, acknowledgements, versions and relevant authorization context. Monitor invariants alongside latency, error rates and availability objectives.

An investigation agent gathers evidence, correlates traces, reproduces failures and proposes patches. Those patches re-enter the same pipeline. Production write access and emergency actions follow an explicit operational policy.