> ## Documentation Index > Fetch the complete documentation index at: https://docs.conseqa.umran.ca/llms.txt > Use this file to discover all available pages before exploring further. # Understanding Verification Verdicts and Proof Status > Conseqa produces three verdicts — proven, unknown, disproven — describing what the verifier can establish from your declared model, not runtime behavior. 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 Confirm that your implementation actually provides the declared facts the proof relies on. The `assumptions` list in the obligation report names them exactly. Read the `evidence` list. Decide whether to declare the missing fact, restructure the operation, or accept the gap. Re-run Conseqa after any change. Inspect the `counterexample` trace. Revise the model or the implementation to eliminate the demonstrated violation. 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.