Skip to main content
Conseqa is a formal model checker for distributed systems. You describe your microservice architecture in a YAML-based DSL — services, schemas, data models, topics, state machines, and operations — and Conseqa’s verification engine statically proves whether your declared correctness requirements hold, reporting each obligation as proven, unknown, or disproven. When you need to share or review a model, conseqa-viz renders it as a single self-contained HTML file with an interactive system graph, per-operation program drill-down, and obligation overlays.

Introduction

Understand what Conseqa does, why it matters, and how its epistemic proof model works.

Quickstart

Write a YAML model, run the verifier, and view your first obligation report in under five minutes.

Core Concepts

Learn about services, schemas, topics, state machines, operations, and requirements.

CLI Reference

Full reference for the conseqa and conseqa-viz command-line tools.

​
How it works

1

Write a YAML model

Describe your architecture using Conseqa’s DSL. Declare services, data models, message topics, and the operations that tie them together — each with explicit requirements for correctness properties you need to hold.
2

Run the verifier

Pass your model to conseqa. Validation checks structural coherence; verification discharges each declared requirement and prints an obligation summary.
3

View the results

Generate an interactive HTML visualization — with obligation status overlaid — and open it in any browser. No server required.
Every verdict is epistemic. unknown means the verifier could not establish the property from the declared facts — it is not evidence of a violation. See Introduction for the full proof model.