# Conseqa

- [Conseqa: Formal Proofs for Microservice Correctness](https://docs.conseqa.umran.ca/introduction.md): Learn what Conseqa is, which correctness properties it verifies, how its epistemic proof model works, and what the two CLI tools do.
- [Get Started with Conseqa in Minutes](https://docs.conseqa.umran.ca/quickstart.md): Install Conseqa, write a minimal YAML model, run the verifier, and generate an interactive visualization — all in a single walkthrough.
- [Installing Conseqa from Source](https://docs.conseqa.umran.ca/installation.md): Build both Conseqa binaries from source using Cargo, add them to your PATH, and verify the installation with the built-in help output.
- [Anatomy of a Conseqa Model](https://docs.conseqa.umran.ca/concepts/model-overview.md): A Conseqa model is a single YAML file with six top-level sections that together describe one snapshot of your distributed architecture.
- [Services, Schemas, and Data Models in Conseqa](https://docs.conseqa.umran.ca/concepts/services-and-schemas.md): Learn how Conseqa models ownership boundaries, value shapes, and persistent object identities using services, schemas, and data models.
- [Operations: The Core Unit of a Conseqa Model](https://docs.conseqa.umran.ca/concepts/operations.md): An operation is a logical unit of behavior in your system. Learn how to declare inputs, effects, transactions, programs, and correctness requirements.
- [Transactions and Atomic Execution in Conseqa](https://docs.conseqa.umran.ca/concepts/transactions.md): Transactions are atomic units inside operations. Learn isolation levels, step kinds, derivation, and how outputs and intents flow into program control.
- [Topics, Ordering, and Message Identity in Conseqa](https://docs.conseqa.umran.ca/concepts/topics-and-messaging.md): Topics are Conseqa's async message channels. Learn how ordering, message identity, delivery, and dispatch routing interact in verification proofs.
- [Modeling State Machines in Conseqa](https://docs.conseqa.umran.ca/concepts/state-machines.md): State machines model persistent lifecycle transitions over data objects. Learn how to declare states, transitions, and side effects in Conseqa.
- [Declaring Correctness Requirements in Conseqa](https://docs.conseqa.umran.ca/concepts/requirements.md): Requirements are proof obligations declared on operations. Learn serialization, ordering, idempotency, and recoverability, plus how verdicts are produced.
- [Conseqa YAML Model Structure Reference](https://docs.conseqa.umran.ca/dsl/model-structure.md): Complete reference for the top-level keys of a Conseqa YAML model: revision, services, schemas, data_models, topics, state_machines, and operations.
- [Field Types and Schema Definitions in the DSL](https://docs.conseqa.umran.ca/dsl/field-types.md): Complete reference for Conseqa's type system: scalar types, optional and list fields, schema references, canonical and fragment schemas, and completeness.
- [Declaring and Using Effects in Conseqa](https://docs.conseqa.umran.ca/dsl/effects.md): Reference for Conseqa's three effect kinds — publication, request, and external — covering idempotency guarantees, retry semantics, and propagation.
- [Operation Program and Control Flow in Conseqa](https://docs.conseqa.umran.ca/dsl/program-control.md): Reference for the operation program field: all step kinds, decision steps, terminal steps, step location notation, and decision replay analysis.
- [Value References and Data Flow in Conseqa](https://docs.conseqa.umran.ca/dsl/value-references.md): Complete reference for ValueRef: seven source kinds, field paths, derivation forms, scope constraints, and how value references underpin keys and replay.
- [How Conseqa Verifies Your Architecture](https://docs.conseqa.umran.ca/verification/how-it-works.md): Conseqa runs two sequential phases — structural validation then correctness verification — and produces epistemic verdicts for each declared requirement.
- [Understanding Verification Verdicts and Proof Status](https://docs.conseqa.umran.ca/verification/verdicts.md): Conseqa produces three epistemic verdicts — proven, unknown, disproven — that describe the strength of evidence for each declared requirement, never runtime observations.
- [The Conseqa Obligations Report Format](https://docs.conseqa.umran.ca/verification/obligations-report.md): Conseqa writes a structured JSON report of every verification obligation — status, assumptions, and evidence — consumable by conseqa-viz and your own tooling.
- [Visualizing Your Architecture with conseqa-viz](https://docs.conseqa.umran.ca/visualization/overview.md): Generate a self-contained, interactive HTML visualization of your Conseqa model — with or without proof results — using the conseqa-viz tool.
- [System View: Architecture Graph in conseqa-viz](https://docs.conseqa.umran.ca/visualization/system-view.md): Explore your full microservice architecture as an interactive SVG graph — services, topics, external systems, and every information route between them.
- [Operation View: Program Flow in conseqa-viz](https://docs.conseqa.umran.ca/visualization/operation-view.md): Drill into any operation to inspect its requirements, inputs, and full program control flow — transaction steps, effect executions, and proof verdicts.
- [State Machine View: Lifecycle Diagrams in conseqa-viz](https://docs.conseqa.umran.ca/visualization/state-machine-view.md): Inspect any state machine as an interactive lifecycle diagram — states, transitions, side effects, and obligation verdicts — with shareable deep links.
- [Modeling a Flash-Sale Checkout with Conseqa](https://docs.conseqa.umran.ca/guides/modeling-a-checkout-flow.md): Build a Conseqa model for a flash-sale checkout service step by step, then run the verifier and interpret its 10 proven and 4 unknown obligations.
- [Proving Idempotency for Distributed Operations](https://docs.conseqa.umran.ca/guides/proving-idempotency.md): Learn how to declare and prove idempotency requirements in Conseqa, using the fully-proven video streaming pipeline as a working example.
- [Integrating Conseqa into Your CI Pipeline](https://docs.conseqa.umran.ca/guides/ci-integration.md): Run Conseqa in CI to catch regressions, fail builds on disproven obligations, and archive proof reports and HTML visualizations as pipeline artifacts.
- [conseqa — Model Validator and Verifier CLI](https://docs.conseqa.umran.ca/cli/conseqa.md): Run conseqa <MODEL.yaml> to validate your architecture model, verify its declared requirements, and print an obligation summary to stdout.
- [conseqa-viz — Architecture Visualization Generator](https://docs.conseqa.umran.ca/cli/conseqa-viz.md): Run conseqa-viz <MODEL.yaml> to generate a self-contained interactive HTML visualization of your architecture, optionally overlaid with proof verdicts.