Verification Verdicts: Proven, Unknown, and Disproven

Every verification obligation Conseqa produces carries one of three verdicts: proven, unknown, or disproven. These are epistemic statements about the declared facts in your model. They describe what the verifier can or cannot establish, not what the running system has been observed to do. Additionally, every proof records its scope (l0_only or runtime_dependent) and the evidence (declarations consumed) that the argument relied on.

​

The Three Verdicts

​

proven

The verifier has established that the declared requirement follows from the facts in your model. The proof names the specific declarations it relies on in the obligation’s assumptions list, and records its scope:

• l0_only — no L1 fact was required. The proof rests entirely on the abstract application machine.
• runtime_dependent — at least one L1 fact was necessary. The proof holds of the declared runtime realization and must be re-examined whenever that realization changes.

A proven verdict is conditional on implementation conformance. If your real implementation does not actually provide the semantics you declared (for example, you declared deduplicated_by but the execution environment does not enforce it), the proof is invalid. Conseqa verifies structure; conformance to the model is your responsibility.

​

unknown

The verifier could not establish whether the property holds. This is the most common verdict for requirements whose proof depends on facts you have not yet declared. unknown arises in several situations:

• A key component that is not sourced from the triggering input (the governing key rule).
• A transaction with idempotency: unspecified or not_deduplicated that the verifier cannot prove naturally replayable.
• An external effect with idempotency: unspecified or not_deduplicated.
• A branch condition that depends on a value the verifier cannot establish as replay-stable.
• A cascade where a downstream consumer’s idempotency is itself unknown.

When you see unknown, read the obligation’s evidence list. It names the specific obstacles: which transaction cannot be resolved, which effect boundary provides no deduplication fact, which decision is not established to replay.

​

disproven

The verifier has found a counterexample — a concrete trace within the declared model that demonstrates a violation of the property. The obligation’s counterexample field contains the trace.

​

Proof Scope

Every proof records the semantic layers its argument consumed: The scope records a dependency, nothing more. A runtime_dependent proof is not weaker in kind; it is conditional on the runtime realization the model declares, and must be re-examined when that realization changes. Changing a pool’s member_concurrency, or dropping a router’s routing block, invalidates the proofs that cited them, and the scope is how a reader finds them. l0_only does not mean implementation-free. A proof resting on isolation: serializable is L0-only, and still assumes the concrete database implements serializable execution. Scope identifies dependency on semantic layers, not the absence of conformance assumptions.

​

Removing L1 Cannot Invalidate a Proof

Deleting the runtime block 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. Conversely, adding L1 to an L0-only model can turn previously unknown obligations into proven (or leave them unknown if the new facts are insufficient). The scope badge on each obligation tells you which category it belongs to.

​

Declarations That Are Not Verdicts

Several DSL values affect what the verifier can infer but are themselves declarations, not verdicts.

​

unspecified

unspecified in any field means: the model provides no fact from which this property may be inferred. It does not mean the property is false. An unspecified fact cannot be used as evidence in any proof, so a proof that would require it produces unknown rather than proven. Examples:

• ordering: unspecified on a topic runtime does not prove messages are unordered.
• member_concurrency: unspecified on a pool does not prove concurrent execution exists.
• idempotency: unspecified on an external effect does not prove repeated calls are unsafe.

​

unordered, unbounded, not_deduplicated

These are explicit negative declarations — stronger than unspecified because they actively assert the absence of a guarantee. Even so, they describe declared guarantees, not necessarily observed runtime behavior:

• unordered says the topic provides no ordering guarantee. It does not mean messages are never delivered in order in practice.
• not_deduplicated on a transaction or external effect says no keyed deduplication is provided. It does not mean every duplicate invocation causes harm at runtime.

The verifier uses these declarations to close proofs that would otherwise be unknown in the negative direction.

​

Coinductive Verdicts

Some proven obligations are marked coinductive in the report. This means the proof was established by greatest-fixpoint analysis over a cycle of mutually dependent requirements. A coinductive proof arises when two or more operations each depend on the other’s idempotency verdict — for example, operation A makes a request to operation B, and B makes a request back to A. The V1 engine assumes all requirements and drops those that fail; a cycle whose members each pass their local checks under the mutual assumption is proven. The coinductive label records that the proof rests on this mutual assumption rather than on independent evidence. Cycles through outboxes are treated identically to cycles through topics or requests; there is no separate outbox solver.

​

Responding to Each Verdict

​

Real Examples

The flash_checkout example model ships with a genuine report that illustrates both outcomes: 10 proven obligations — including serialization, ordering, and recoverability for apply_payment and create_order, and result replay for create_order. These operations use keyed commits, identified events, and subscription dispatch with routing.key: grouping_key, member_assignment.kind: consistent_hash, and member_concurrency: { kind: bounded, value: 1 } on the target pool. 4 unknown obligations — including idempotency for reserve_inventory, charge_payment, and create_order. The root causes:

• tx.reserve_inventory is declared not_deduplicated and its mutation depends on a transaction read, so neither the recovery nor the reconstruction route is available.
• The external card charge (effect.charge_payment.card) is declared not_deduplicated, which means no same-key terminal result is fixed. The match_result on the card result is therefore not established to replay, because a retry may observe a different outcome.
• create_order’s idempotency cascades through the OrderCreated event to reserve_inventory, whose idempotency is itself unknown.

The video_streaming example model is designed to be fully proven. Every operation uses a keyed commit, every external effect declares deduplicated_by, and the transcoding engine’s error disposition is declared terminal, which fixes the result for retries and allows the match_result to replay.