Conseqa: Formal Proofs for Distributed Correctness

Conseqa is a formal model checker for distributed microservice architectures. You describe your system in a YAML-based DSL with hierarchical semantics: services, operations, transactions, effects, topics, state machines, and the correctness properties each operation must satisfy live at the application layer, and an optional topology layer sits above it to describe how the architecture is realized. Each layer is meaningful on its own and composes with the other. The verifier analyzes what you declared and produces epistemic verdicts, proven, unknown, or disproven, for every requirement. The application layer is a logical description of the system, deliberately independent of any particular deployment. When you need to reason about how the architecture actually scales, you layer runtime topology on top: routing, pool concurrency, transport ordering, storage partitioning, and outbox dispatch. That topology is optional, and when present it may also participate in proofs whose conclusions depend on it.

​

Correctness properties Conseqa verifies

Conseqa focuses on five families of correctness obligations at the operation level:

• Idempotency. Repeated attempts representing the same logical invocation must not cause externally distinguishable duplicate work. Proved across the full cascade: transactions, publications, outbound requests, external effects, and outbox writes.
• Result replay. For requirements that declare result: replay_consistent, repeated attempts in the same idempotency class must return the same result variant and replay-equivalent payload.
• Serialization. Same-key invocations must not execute concurrently.
• Ordering. Same-key invocations for which a meaningful logical precedence exists must preserve that precedence through execution.
• Recoverability. The logical invocation must reach a valid terminal after any modeled interruption. A progress obligation, distinct from idempotency.

​

What you declare

At the model root you describe the application itself: services, schemas, data_models (including any typed outboxes owned by a data model), topics, state_machines, and operations. Each operation names its invocation sources (request, subscription, or outbox), spells out one explicit causal program, and lists the requirements it must satisfy. This description stands on its own: the verifier can validate structural coherence and discharge many correctness obligations from these facts alone. Some obligations, particularly ones about ordering, serialization under contention, and recoverability under redelivery, only close once you also describe how the architecture runs. For that, an optional runtime block declares realization facts: execution pools with member_concurrency, routers that assign requests onto pools, transport grouping and ordering, subscription and outbox delivery and dispatch, and storage layouts. These declarations serve two audiences: the verifier, which may consume them to close proofs, and an external quantitative analysis (hot members, routing skew, queue growth, pool sizing) that reads the same declarations at scenario time. Runtime declarations are qualitative; numbers like member counts and traffic rates stay outside the model. Every proof records which declarations it consumed, so it is always clear what a verdict rests on and what would change it.

​

The three verdicts

Every obligation comes back proven, unknown, or disproven:

​

The two CLI tools

conseqa validates the YAML model and verifies its requirements. Validation errors are fatal; verification proceeds only over a coherent model. After verification, it prints a summary and optionally writes a JSON obligation report. conseqa-viz renders the model as a single self-contained HTML file with a system graph, per-operation program drill-downs, and state-machine views. Pass --verify to overlay proof verdicts, or --report to overlay a previously produced report.