Skip to main content
Conseqa describes a logical architecture: an abstract application machine and an optional runtime realization layered on top of it. A model is not deployment configuration and not executable code. It is a declaration that a verifier can analyze for structural coherence and correctness.

​
Hierarchical semantics: application, then topology

The DSL is layered. Every declaration belongs to exactly one of two layers, and each layer is meaningful on its own: The governing rule is: L0 says what application machine exists and what properties it requires. L1 says how invocations and persistent data are arranged in a particular runtime realization of that machine. L1 is optional. An L0-only model is complete, structurally valid, and analyzable. Removing L1 from a valid model never makes it invalid: it only makes proofs that consumed runtime facts unavailable. The verifier records the scope of every proof it produces: l0_only when no L1 fact was required, or runtime_dependent when at least one was necessary.
A runtime_dependent proof is not weaker in kind; it is conditional on the declared realization, and must be re-examined when that realization changes.

​
The seven L0 root collections

A model root contains these top-level keys:
  • services : Logical ownership and grouping boundaries for operations. Kinds are descriptive only (backend, frontend, worker, job); a service does not imply a process boundary, network hop, replica count, or trust boundary.
  • schemas : Canonical and fragment schemas that describe the logical shape of values. Includes scalar types, lists, optional flags, and field-path shorthand.
  • data_models : Logical transactional state boundaries containing persistent objects and outboxes.
  • topics : Logical message channels that declare which schemas they may carry and what identifies one logical message. See Topics and messaging.
  • state_machines : Legal states and transitions for a persistent object field. Each transition may declare shared side-effect contracts.
  • operations : Logical units of application behavior with inputs, a single acausal program, and requirements. See Operations.
  • revision : An opaque numeric revision marker for the model snapshot. The current DSL assigns no ordering, compatibility, or migration semantics beyond numeric identity.

​
What belongs in L1

When runtime is present, it may contain:
  • topics : TopicRuntime declarations with optional grouping and ordering.
  • subscriptions : SubscriptionRuntime declarations per (operation, input) pair, covering delivery, grouping, ordering, and dispatch.
  • outboxes : OutboxRuntime declarations per (operation, input) pair, covering delivery, partitioning, ordering, dispatch, and batching.
  • execution_pools : Logical populations of interchangeable runtime members with member_concurrency.
  • routers : Request routing from a boundary to a pool, with an optional semantic routing key.
  • storage_layouts : Physical partition identity for a DataObject.
Grouping and ordering are declared at exactly one of two scopes for a given topic: either once at the topic runtime, or independently at each subscription runtime. They are never declared at both. There is no inheritance, no override, and no fallback chain. See Topic and subscription runtime.

​
Semantic categories

Independently of layer, a declaration belongs to one of three categories: A structurally valid model is therefore not necessarily a safe model. Validation establishes that declarations are coherent and references are meaningful. Verification establishes whether the declared requirements follow from the declared facts and architecture.

​
unspecified is epistemic

Across the DSL, unspecified means:
The model provides no fact from which the corresponding property may be inferred.
It does not mean that the property is false, and it does not mean the implementation is allowed to violate a requirement. It means the verifier must treat the fact as unknown. An unknown fact cannot be used as evidence for a proof. For example, ordering: unspecified does not prove messages are unordered. concurrency: unspecified does not prove concurrent execution exists. idempotency: unspecified does not prove an external effect is non-idempotent.

​
Removing runtime facts

Deleting the runtime model from a valid model leaves it valid. Requirements discharged from runtime facts become unproven (never violated, and never a structural error). That asymmetry is the point of the layering: L0 stands alone, and L1 is what a particular realization adds. For the full runtime vocabulary, see Runtime overview.