Version: 0.1 Canonical Draft
Status: Normative pilot specification
This specification defines a language-agnostic and agent-agnostic structure for reliable modular software.
It standardizes semantic boundaries, contracts, ownership, effects, operational semantics, compatibility, and conformance. It does not prescribe a programming language, framework, deployment topology, persistence model, or coding agent.
The key words MUST, MUST NOT, SHOULD, SHOULD NOT, and MAY indicate requirement levels.
An RMS-compliant system SHOULD make it possible to:
- understand a module without reading unrelated implementation code;
- change or replace a module through its public contract;
- detect undeclared dependencies and effects;
- reason about retries, concurrency, failure, and recovery;
- provide agents with bounded, trustworthy context;
- enforce important rules independently of prompt compliance;
- implement the same semantic contract in different languages.
A repository or deployable system MAY be modeled as a system module. A system module defines the public boundary, contained contexts, external dependencies, system-wide invariants, and runtime composition.
A bounded context is a semantic boundary within which one domain model and vocabulary are authoritative. A context MUST own its domain meaning and MUST NOT expose private domain objects as shared mutable state.
A module is a cohesive unit of meaning and ownership with an explicit public contract. Modules MAY be nested. A nested module MUST preserve the public/private boundary of its parent.
A composite module MAY declare contained submodules and public exports backed by those submodules. A submodule marked internal MUST NOT be consumed directly from outside the parent boundary; external consumers MUST depend on the parent export or on a submodule explicitly marked public.
An aggregate is a boundary of immediate consistency and invariant enforcement. An aggregate SHOULD be no larger than the state that must change atomically.
A workflow coordinates several modules or aggregates over time. It owns coordination state but MUST NOT bypass the invariants or private state of participating modules.
The kernel contains small, stable technical primitives shared across modules. The kernel MUST NOT become a repository-wide business model or communication mediator.
A contract defines a public command, query, event, capability, API, or data exchange. A contract includes semantic and operational behavior when those properties affect consumers.
Contract publication MUST identify its kind and direction. Provided command, query, event, and capability contracts extend the matching public collection. Required contracts MUST be capabilities and extend the module's required capability collection. Publishing or requiring a capability MUST NOT imply a module split or recursive topology.
An effect is contact with state or reality outside a pure decision boundary, including storage, network calls, time, randomness, messaging, filesystem access, secrets, or external services.
A derived fact is computed from accepted state and other accepted facts. It MUST NOT create new source-of-truth state by itself.
A module package is a transport-neutral distribution of a public module. It contains the semantic manifest, published contracts, required conformance material, and enough implementation or endpoint information to use or evaluate the module.
A conformance report is machine-readable evidence that a particular system or module implementation was evaluated against a named RMS version, profile set, source revision, implementation binding, and validator version.
A semantic function is an implementation-level function, method, parser, constructor, transition, adapter, or interpreter that carries a named part of a module's declared meaning.
Semantic functions MAY be declared by an implementation binding to connect public contracts, invariants, assumptions, and verification evidence to concrete source symbols. A semantic function declaration MUST NOT create public meaning that is absent from the module manifest or published contracts.
Intent is the human-facing statement of why behavior is wanted, including stories, examples, counterexamples, open questions, accepted answers, and rejected interpretations.
Rationale is the accepted explanation for why a particular interpretation, contract, invariant, ownership boundary, compatibility choice, or proof lane was chosen.
Intent and rationale MAY be recorded as natural-language artifacts and linked from manifests, contracts, laws, or evidence. They explain and justify public meaning, but they MUST NOT silently override manifests, contracts, invariants, context language, compatibility declarations, or verification evidence.
Architecture-sensitive work MUST begin with a validated structured intent model or an explicit clarification result. The model MUST classify domain decisions, lifecycle, effects, runnable surface, and reuse as required, absent, or unknown. Explicit facts MUST retain an exact source quote. Inferred facts MUST retain a rationale. Material unknowns MUST stop topology selection.
An intent model MUST NOT contain module names, semantic shapes, topology, or scaffold recommendations. Agents and providers MAY extract the model. Deterministic RMS policy MUST choose topology from validated facts. The resulting canonical module, contract, implementation, and evidence artifacts remain authoritative.
An implemented RMS module MUST declare a domain-named semantic machine. Binding-native container names MUST be declared separately from semantic alternatives. A machine's state, command, observed-event, event, effect, effect-result, reply, and rejection lists MUST contain case names rather than the names of their enclosing language types.
Stateful, boundary, workflow, storage, integration, and projection machines MUST expose one canonical transition that consumes current state plus a closed input over commands, observed events, and effect results. Each transition input MUST belong to exactly one category. Stateless decision machines MAY consume input without state only when an explicit justification explains why no lifecycle or ordering exists.
A declared effect MUST define its possible results and atomicity. A module that executes the effect MUST declare its executor role. A pure request provider MAY instead select an explicitly supported caller-driven binding. That provider MUST retain typed request/result protocols and MUST NOT declare local execution authority. The caller owns execution; provider proof MUST NOT claim to certify caller IO. When an individual result can alter a subsequent decision, the protocol MUST use one request and one result, and that result MUST return through the canonical transition. Effect executors MUST NOT own business sequencing, iteration, retry, compensation, stop/continue policy, or machine state progression.
An RMS workspace declares progressive or complete coverage. Progressive coverage certifies discovered RMS modules and their declared dependency closures only. Complete coverage claims the repository production surface and MUST fail while production paths remain outside RMS ownership.
Module-scoped production checks MUST include contained children and transitive declared module providers. Dirty or unresolved paths inside that closure invalidate the proof. Unrelated out-of-scope paths MUST be reported without being represented as part of the certified closure.
Every declared RMS module MUST satisfy the Core profile. Ordinary private components need not be modeled as separate RMS modules.
A module that is public across an ownership boundary, independently replaceable, separately deployable, or claimed as an RMS conformance subject MUST declare:
- a stable name;
- a version;
- a concise purpose;
- its kind or role;
- its owning context or system boundary when applicable.
A bounded context MUST define its authoritative domain terminology. A system glossary MAY index terms across contexts but MUST NOT override context-local meanings.
Normative natural-language semantic statements SHOULD use ASD-STE100 rules as a controlled-language baseline. Each sentence SHOULD state one obligation, condition, or result, name its subject explicitly, and use one canonical term for each concept. Bounded-context terms, exact identifiers, schema keys, formulas, and quoted contract language take precedence over the controlled-language vocabulary. Controlled-language rules MUST NOT weaken semantic precision or compatibility.
A module MUST declare the concepts, state, data, and business decisions it owns.
A module MUST NOT modify another module's private state directly.
A module MAY request work through a public command or capability and MAY consume information through a public query or event.
Owned semantic state SHOULD NOT be exposed as shared mutable state. Changes to owned semantic state SHOULD enter through the owner boundary as commands, accepted facts, or declared transition functions.
A module MUST distinguish its public contracts from its private implementation.
Private implementation includes, unless explicitly published:
- internal tables or storage layouts;
- internal helper functions;
- vendor SDK objects;
- framework-specific objects;
- internal domain events;
- mutable entity instances.
Consumers MUST depend only on published contracts.
When a parent module exports behavior implemented by a child module, the parent MUST publish the exported contract and the child MUST provide the backing command, query, event, or capability. The export does not make the child's private implementation public.
A module MUST declare required modules, contracts, and capabilities.
Undeclared dependencies MUST be rejected by conformance tooling when the implementation binding can detect them.
Circular dependencies SHOULD be eliminated. When a semantic cycle is unavoidable, the shared concept SHOULD be extracted or interaction SHOULD be mediated by a contract or workflow.
A module MUST declare the important properties that must remain true.
An invariant SHOULD have:
- a stable identifier;
- a plain-language statement;
- an enforcement location;
- verification evidence.
An invariant MUST declare its authority as representation, constructor, parser, transition, effect executor, or composition. Lifecycle, sequencing, retry, compensation, and progress invariants MUST have transition authority. An effect executor MAY enforce IO mechanism rules but MUST NOT discharge transition-authority laws.
Invariants SHOULD be few, meaningful, and owned by the narrowest valid consistency boundary.
A module MUST declare externally observable effects and required effect capabilities.
Effects SHOULD be isolated behind explicit ports, capabilities, or interpreters.
Ambient access to global state, network, storage, time, randomness, or secrets SHOULD be minimized and MUST NOT bypass declared permissions.
Effect handlers SHOULD execute one declared request and return one declared observation, failure, timeout, or acknowledgement through an effect result. They MUST NOT make cross-module domain decisions, mutate another module's owned semantic state, or hide iteration and progress policy that belongs in a transition.
A public contract MUST use rms/contract/v0.2 and define domain meaning as an executable, language-neutral relation over typed input, output, before/after state, transitions, protocol observations, trace metrics, events, effects, and rejection outcomes as applicable.
Command, query, and capability contracts MUST declare typed observations, caller requirements, guarantees, invariants, exhaustive behavior cases, accepted or rejected outcomes, and permitted state/event/effect frames. Event contracts MUST declare typed payload observations and guarantees. API contracts MUST close over exact command, query, event, or capability contract references. Existing protocol semantics MAY coexist with behavioral semantics.
Each behavioral clause MUST have a stable identifier, a human statement, and exactly one realization: a portable RMS core expression or one exact executable external property identifier. unresolved MAY appear only in a generated migration draft and MUST fail strict conformance. RMS core expressions MUST remain closed, exactly typed, and free of host callbacks, arbitrary code, floating-point semantics, textual parsing, and unbounded quantification.
Case coverage MUST be exhaustive and overlap MUST be forbidden unless intentional nondeterminism explicitly permits it. A query MUST have an empty state, event, and effect frame.
Evaluation MUST apply the relation:
invariants(before) ∧ requirements(input, before)
⇒ permitted case/outcome ∧ guarantees ∧ invariants(after)
A requirement violation assigns caller blame. A postcondition, frame, or invariant violation assigns provider blame. A malformed or incomplete record assigns binding/evidence blame. A declared rejected outcome is normal contract behavior.
When relevant to consumers, a contract MUST also define:
- preconditions and postconditions;
- failure categories;
- authorization expectations;
- observability or causal identifiers when required by consumers;
- idempotency;
- ordering scope;
- consistency expectations;
- timeout and retry semantics;
- versioning and compatibility policy;
- service constraints when consumers depend on latency, throughput, availability, payload, resource, or cost bounds.
Stateless calls MUST be observable as rms/invocation-record/v0.1; stateful behavior MUST use transition records. Binding-specific tests MAY invoke native code and emit these records, but MUST NOT replace the RMS evaluator with generated host-language predicates or wrappers.
Compatibility MUST preserve the old valid input domain, constrain new behavior for old-valid inputs to the old permitted relation, and keep new events, effects, rejection outcomes, and state changes within the old frame. Concrete refinement counterexamples are breaking; proven input-domain expansion is additive; unsupported or external obligations require operational review unless exact digest-bound external refinement evidence discharges them.
Modules MAY communicate by direct in-process calls, commands, queries, events, or capabilities.
Communication MUST cross the provider's public contract.
A query MUST NOT perform hidden domain mutation.
An event MUST represent a fact accepted by its owning module. An instruction disguised as an event SHOULD be modeled as a command.
When asynchronous host inputs feed domain behavior, adapters SHOULD normalize them into typed commands, events, or boundary values before domain decisions are made. Ordering-sensitive behavior SHOULD declare and honor an ordering scope.
Business decisions SHOULD depend on owned state and derived facts, not on scattered direct reads of unrelated private state across module boundaries.
Semantic representations SHOULD be immutable by default. A semantic state update SHOULD be expressible as an accepted input plus prior state producing a next state, derived facts, accepted or rejected results, and requested effects.
Localized mutation MAY be used inside an implementation for construction, caching, performance, I/O, or host-runtime integration when it does not leak shared mutable semantic state across the module boundary and preserves the declared contracts, invariants, and operational semantics.
State transitions that affect public behavior SHOULD be explicit semantic functions or equivalent language-native constructs. Illegal states and illegal transitions SHOULD be rejected or made unrepresentable through closed variants, validated constructors, schemas, state models, or transition functions.
A module MUST declare a compatibility policy for public contracts.
Breaking changes MUST be explicit and versioned. A migration or coexistence path SHOULD be provided for active consumers and owned state.
Implementation details MAY change without a public version change when declared behavior remains compatible.
A module MUST declare verification evidence in the following categories as applicable:
- laws: invariants, state rules, and algebraic properties;
- contracts: provider, consumer, schema, and adapter compatibility;
- scenarios: meaningful behavior and recovery paths;
- boundaries: validation of untrusted or versioned input.
A module MUST NOT be required to use every testing technique. The chosen evidence MUST be proportional to risk and strong enough to demonstrate the declared promise.
A module MUST declare the operational mechanisms required by its profiles and effects.
When relevant, this includes:
- causal identifiers and observability;
- runtime invariant checks;
- reconciliation and repair;
- migration and rollback procedures;
- runbooks and manual-review paths.
Operational mechanisms MUST use the same public semantics and ownership boundaries as the implementation.
An implementation binding MAY declare semantic functions that map source symbols to module invariants, public contracts, assumptions, and evidence.
Semantic function bindings SHOULD classify the source symbol using the smallest accurate role:
- constructor: raw or internal input to a validated value;
- parser: untrusted or versioned input to a boundary value;
- decision: state and intent to a pure domain decision;
- transition: state and accepted fact to new state;
- projector: fact to read model;
- adapter: external model to or from domain model;
- interpreter: effect request to external result.
For each semantic function, a binding SHOULD identify whether its assumptions are:
- represented by input or output types;
- checked as preconditions;
- preserved as invariants;
- guaranteed as postconditions;
- demonstrated by verification evidence.
Pure semantic functions SHOULD be deterministic for the same accepted inputs and SHOULD NOT perform undeclared effects. Effectful semantic functions MUST remain within the module's declared effects and required capabilities.
The manifest and public contracts MUST be updated when public meaning, ownership, dependencies, effects, or compatibility changes.
Agent instruction files MUST NOT be the sole source of architectural truth.
Canonical semantic artifacts MUST agree. A contradiction among manifests, contracts, invariants, context language, or compatibility declarations is a conformance failure and MUST NOT be resolved by an agent through an undocumented precedence choice.
When intent or rationale records are used, they SHOULD evolve with semantic changes. A change that alters accepted behavior SHOULD update or supersede the linked intent, decision, contract, law, and evidence records as one coherent semantic trace.
Implementation work SHOULD be preceded by intent capture when the requested behavior changes public meaning, ownership, lifecycle rules, source of truth, compatibility, external effects, recovery behavior, or proof obligations.
Manifests, public contracts, conformance reports, and agent context packets MUST NOT contain credentials or production secrets.
Executable agent extensions, hooks, plugins, and validation tools SHOULD be version-pinned, reviewable, and granted the least capabilities needed for their task. Their behavior MUST NOT redefine RMS semantic truth.
A module MUST declare each additional profile whose conditions apply.
The Stateful profile applies when a module owns a lifecycle or transactional consistency boundary.
The module MUST additionally declare:
- state model or lifecycle;
- legal transitions;
- consistency and transaction boundary;
- concurrency policy;
- representation and mutation policy;
- persistence and migration policy.
Illegal transitions MUST be rejected or made unrepresentable.
When lifecycle behavior depends on event or command order, transitions SHOULD be reducible over an ordered input stream within the module's consistency boundary. Stale, duplicate, or out-of-order observations SHOULD be rejected, ignored, or reconciled according to declared operational semantics.
The Distributed profile applies when behavior crosses a process, network, durable queue, or external vendor boundary.
The module MUST additionally declare:
- delivery semantics;
- idempotency strategy;
- ordering scope;
- timeout interpretation;
- retry policy;
- duplicate handling;
- partial-failure behavior;
- reconciliation or repair mechanism when external truth can diverge.
When a local state change and message publication must be atomic, the implementation MUST use an outbox, transactional log, or an equivalent mechanism.
At-least-once delivery MUST be paired with idempotent consumption or an equivalent duplicate-control mechanism.
The Workflow profile applies to long-running coordination across modules or aggregates.
The workflow MUST additionally declare:
- trigger and completion conditions;
- coordination state;
- deadlines and timeouts;
- failure and terminal states;
- compensation or repair paths;
- manual-review states when automatic resolution is unsafe;
- replay or resumption behavior.
A workflow MUST use public contracts and MUST NOT mutate participant-owned state directly.
The Boundary profile applies where untrusted or versioned data crosses a system or context boundary.
The module MUST additionally declare:
- accepted schema and versions;
- input validation;
- trust and authorization boundary;
- resource limits where relevant;
- malformed-input behavior;
- compatibility and deprecation policy.
Boundary verification SHOULD include semantic fuzz properties or generated adversarial cases when parser complexity or security risk justifies it. The semantic property SHOULD name the raw input space, parse/delegation oracle, evidence path, replayable counterexample policy, and realization strategy. A fixed deterministic corpus MUST NOT satisfy an open-ended fuzz claim. Complete finite spaces MAY use deterministic exhaustive evidence; open spaces require generated-property or coverage-guided evidence for a production claim.
Implemented modules MUST declare strong verification lanes derived from their semantics: generated or exhaustive properties for pure and numeric decisions; finite exploration for stateful machines and workflows; coverage fuzzing for untrusted boundary, parser, storage, and external-result input; deterministic schedule and fault exploration for distributed behavior; static analysis or sanitizers for unsafe, foreign, or privileged authority; mutation testing for important reusable semantic oracles; and real-trace evaluation plus violation search for temporal promises.
A module MAY declare a closed verification.hunt_exceptions item only when the named obligation is genuinely inapplicable, and MUST give a focused reason. Fast candidate checks validate that posture but do not require a fresh expensive campaign. rms hunt executes declared nightly lanes in an isolated committed checkout and records bounded evidence. Only exhausted finite exploration MAY support a universal finite conclusion; fuzzing, sanitizers, generated cases, bounded search, and mutation testing MUST NOT be described as global proof. Every retained behavioral failure MUST be replayable.
Behavioral-contract analysis MUST check satisfiability, vacuity, case coverage and disjointness, contradictory guarantees, and frame consistency when the core theory supports them. Solver exchange MUST be deterministic SMT-LIB v2. cvc5 is the reference external solver and MUST remain optional rather than linked or bundled. Solver evidence MUST record identity, version, input digest, timeout, result, model, unsat core, and RMS model revalidation. Missing solvers, timeout, unknown, or unsupported theories are unresolved, never successful. Every satisfiable model used as a counterexample MUST be re-evaluated by the RMS reference evaluator.
The Monitor profile applies when a module observes runtime inputs over time to compute derived facts, check envelopes or invariants, and emit findings, events, or declared supervisory commands.
The module MUST additionally declare:
- observed inputs and their source contracts or capabilities;
- temporal semantics such as ordering, sampling, clock, or history window when relevant;
- derived facts or streams used for monitor decisions;
- trigger conditions and emitted outputs;
- monitor authority: observe-only, advisory, enforcing, or fail-safe;
- idempotency, cooldown, or retrigger policy when triggers can repeat;
- fail-open, fail-closed, or degraded-mode behavior.
rms property monitor is an out-of-process, fail-open observer. Production violations and coverage gaps MAY be logged or exported but MUST NOT control the application result. Missing observations are coverage gaps, never passing evidence. Test and CI evaluation lanes MUST fail on violations independently of production monitoring.
A monitor MUST NOT mutate controlled module state directly. Supervisory behavior MUST cross public contracts as commands, events, alarms, findings, or capabilities owned by the receiving boundary.
Monitor verification SHOULD include trigger and non-trigger cases, stale or out-of-order observations when relevant, and failure-mode evidence for the declared authority.
RMS does not require event sourcing.
A module MAY persist current state, an event log, or both. The choice MUST be consistent with its declared audit, replay, migration, and recovery needs.
A module using events MUST distinguish internal domain events from public integration events when internal evolution would otherwise break consumers.
Published events MUST be versioned or governed by a compatibility policy.
Event-sourced and current-state implementations SHOULD still expose deterministic transition semantics for ordered accepted inputs when stateful behavior depends on lifecycle or order. The persisted representation MAY differ from the semantic model when adapters preserve the declared contracts, invariants, and recovery behavior.
An implementation MAY claim substitutability for another implementation only when it:
- provides compatible public contracts;
- requires compatible capabilities;
- preserves the declared invariants;
- provides compatible operational semantics;
- passes the same required conformance suite;
- supports required state migration or import/export behavior;
- satisfies declared service constraints that consumers rely on.
Schema compatibility alone is insufficient for a substitutability claim.
The semantic manifest MUST NOT require a specific programming-language construct.
Language-specific source locations, build commands, package metadata, and static-analysis configuration MUST be placed in an implementation binding rather than the semantic module manifest.
A compliant project MUST NOT require a specific coding agent.
Vendor-specific instructions, skills, plugins, hooks, and MCP integrations MAY adapt the system for an agent but MUST NOT alter the semantic meaning of the manifests or contracts.
Prompt files MAY guide agent behavior. Deterministic constraints MUST be enforced through tooling, permissions, hooks, CI, runtime checks, or equivalent mechanisms.
Conformance MUST depend on the resulting artifacts and evidence, not on which person or agent produced them. Agent-generated changes SHOULD produce the same reproducible build, verification, compatibility, and provenance evidence required of any other change.
A compliant system MUST provide a system manifest or equivalent machine-readable artifact.
Every public module MUST provide a module manifest or equivalent machine-readable artifact.
The canonical exchange format in this draft is YAML. JSON MAY be used when it preserves the same data model.
Manifests MAY contain extension fields prefixed with x-. Extensions MUST NOT weaken core requirements or silently change the meaning of standard fields.
A module package MAY be distributed as a directory, archive, language package, registry artifact, container, or remote-service descriptor. RMS does not prescribe the transport.
A public package claiming RMS compatibility MUST include or reference:
- its module manifest;
- all published contracts;
- required conformance suites or acceptance criteria;
- an implementation binding or endpoint descriptor;
- compatibility and deprecation information;
- migration or import/export behavior when state replacement is claimed.
A module package MAY omit source code. Consumers MUST NOT depend on package contents declared private.
A conformance claim MUST identify:
- the RMS specification version;
- the module or system being evaluated;
- declared profiles;
- implementation binding;
- validator or conformance-suite version;
- source revision or artifact digest;
- result and evidence location;
- individual pass, fail, skipped, and not-applicable outcomes.
Core conformance requires:
- valid manifests;
- declared ownership and public contracts;
- declared dependencies and effects;
- no detectable private-boundary violations;
- verification evidence for declared laws and contracts;
- compatibility policy;
- all declared profile requirements;
- consistency among canonical semantic artifacts;
- no secrets in canonical artifacts or context packets.
A project MAY be partially conformant during migration but MUST label missing requirements explicitly.
RMS does not mandate:
- microservices;
- event sourcing;
- command/query segregation at deployment level;
- functional programming;
- a particular directory layout;
- repositories or service classes;
- formal verification everywhere;
- one testing technique per category;
- one global domain model;
- one coding agent or plugin platform;
- one package manager, registry, archive, or deployment transport.
The conceptual core of modules, ownership, contracts, invariants, effects, profiles, composition, substitutability, and conformance is frozen for the 0.1 pilot and intended to remain stable.
Manifest syntax, schemas, language bindings, tool commands, and agent integrations MAY evolve on independent version tracks.