Skip to main content
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.

​
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 — topic ordering, dispatch routing, transaction isolation, keyed commit deduplication, external idempotency guarantees, and so on — in the obligation’s assumptions list. 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 what you declare, not what you build.

​
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 is not a violation. It is not evidence that the property fails at runtime. It means the declared model does not contain enough information for the verifier to produce a proof. Treating unknown as a red flag to fix immediately — rather than a gap to inspect and decide about — will produce incorrect conclusions.
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.
In the current V1 engine, disproven obligations are reserved in the format and may appear in future releases. The present engine raises unknown rather than disproven for gaps it cannot close.

​
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 does not prove messages are unordered.
  • concurrency: unspecified on an operation does not prove unbounded concurrency.
  • 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 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. For example, not_deduplicated on an external effect causes any idempotency requirement that reaches that effect on a retryable path to be unknown — the gap is now explicitly declared rather than merely absent.

​
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.
Coinductive proofs are sound. The minimal-counterexample argument in the semantics contract establishes that a self-consistent set of requirements cannot contain an actual violation. The label is informational — it tells you the proof structure, not that the proof is weaker.

​
Responding to Each Verdict

proven

Confirm that your implementation actually provides the declared facts the proof relies on. The assumptions list in the obligation report names them exactly.

unknown

Read the evidence list. Decide whether to declare the missing fact, restructure the operation, or accept the gap. Re-run Conseqa after any change.

disproven

Inspect the counterexample trace. Revise the model or the implementation to eliminate the demonstrated violation.

coinductive

Verify that the mutually dependent cycle in your architecture is genuinely self-consistent — each operation in the cycle really does collapse duplicates from the others.

​
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 by_topic_key dispatch with bounded(1) lane concurrency. 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.