Covenant

A DSL for verified smart contracts with compile-time state machines, written entirely in Haskell.

▶ Try it in your browser: Covenant Playground — write a contract and watch it get verified live. The compiler runs client-side, compiled to WebAssembly — no server.

Covenant is a small, safe language for describing digital agreements. Its compiler front-end proves properties about a contract before it ever runs:

• No illegal state transition is possible (you can't release funds from a contract that was never funded).
• All types are consistent (you can't add a Token to an Address).
• Every declared state is reachable, and the machine has no accidental deadlocks.

The output is a verification report (human-readable or JSON). Covenant does not compile to bytecode — the focus is the compiler front-end (lexing, parsing, type-checking, state-machine verification), which is where Haskell's type system and parser combinators shine.

---

The language

-- A simple escrow contract
contract Escrow {
  state: Draft -> Funded -> Released | Disputed

  party buyer  : Address
  party seller : Address
  value amount : Token

  transition fund(from: buyer, value: amount) {
    require state == Draft
    move -> Funded
  }

  transition release(from: buyer) {
    require state == Funded
    transfer amount -> seller
    move -> Released
  }

  transition dispute(from: buyer) {
    require state == Funded
    move -> Disputed
  }
}

---

Language guide

A contract is a state machine plus the participants, values, and transitions that move between its states.

Construct	Example	Meaning
State machine	state: Draft -> Funded -> Released | Disputed	The states, from initial to final. -> is a step; | lists alternatives.
Party	party buyer : Address	A participant — always an Address.
Value	value amount : Token	A token amount the contract holds.
Transition	transition fund(from: buyer) { … }	A named, guarded move. from: is the caller.
Guard	require state == Draft	A precondition — which state the transition applies from.
Transfer	transfer amount -> seller	Move a token to a party.
Move	move -> Funded	Advance to the next state.

From this, the compiler proves that every declared state is reachable, no reachable state deadlocks, and every reference and type is consistent — all at compile time, before the contract runs.

---

Architecture

Covenant is a classic compiler front-end pipeline:

flowchart LR
    A["Source (.cov)"] --> B["Lexer"]
    B --> C["Parser"]
    C --> D["AST"]
    D --> E["Type Checker"]
    E --> F["State Verifier"]
    F --> G["JSON / text report"]

Loading

Phase	Module	Responsibility	Haskell technique
Lexing & parsing	Covenant.Lexer, Covenant.Parser	Source text → AST	Megaparsec (scannerless parsing)
Syntax	Covenant.Syntax, Covenant.Syntax.Pretty	AST + pretty-printer	ADTs, newtype-tagged names
Type checking	Covenant.TypeCheck, Covenant.TypeCheck.Env	Static type rules	ReaderT / StateT / ExceptT
State verification	Covenant.StateMachine	Reachability & deadlocks	Graph traversal, Data.Map/Data.Set
Output	Covenant.Emit, Covenant.Error	JSON report + errors	Aeson (deterministic JSON)

---

Quick start

With Nix (reproducible)

nix develop            # drops you into a shell with GHC + cabal + HLS
cabal test             # 50 tests
cabal run covenant -- verify examples/escrow.cov

Or build the binary directly:

nix build
./result/bin/covenant verify examples/escrow.cov

With cabal (if you already have GHC 9.6)

cabal build all
cabal test all
cabal run covenant -- verify examples/escrow.cov

---

Using the CLI

Covenant exposes each compiler phase as a subcommand:

covenant lex    examples/escrow.cov   # print the token stream
covenant parse  examples/escrow.cov   # print the parsed AST (re-rendered)
covenant check  examples/escrow.cov   # run the type checker
covenant verify examples/escrow.cov   # full pipeline + state-machine report

A sound contract:

$ covenant verify examples/escrow.cov
[OK] examples/escrow.cov verified.

  reachable states: Disputed Draft Funded Released
  terminal states:  Disputed Released

A broken one — an unreachable state and a deadlock, caught at compile time:

$ covenant verify examples/deadlock.cov
[FAIL] State machine verification failed:
  unreachable states (cannot be reached from the initial state): `Disputed`, `Released`
  deadlock states (reachable, not final, but with no way out): `Locked`

Machine-readable output for CI pipelines:

covenant verify --format json examples/escrow.cov

{
  "contract": "Escrow",
  "reachability": {
    "deadlocks": [],
    "reachable": ["Disputed", "Draft", "Funded", "Released"],
    "terminals": ["Disputed", "Released"],
    "unreachable": []
  },
  "verification": { "ok": true, "errors": [] }
}

---

What the compiler verifies

• Types — parties are Address, values are Token; transfer moves a Token to a party; require compares operands of the same sort (so require state == amount is rejected).
• References — from: names an existing party, move targets a declared state.
• State machine — every declared state is reachable from the initial state; no reachable, non-final state is a dead end.

---

Project layout

covenant/
├── app/Main.hs               -- CLI entry point
├── src/Covenant/
│   ├── Lexer.hs              -- lexeme primitives + standalone tokenizer
│   ├── Syntax.hs             -- surface AST
│   ├── Syntax/Pretty.hs      -- AST pretty-printer (re-parseable)
│   ├── Parser.hs             -- scannerless parser (Text → AST)
│   ├── Error.hs              -- unified error types + renderers
│   ├── TypeCheck.hs          -- type checker (monad-transformer stack)
│   ├── TypeCheck/Env.hs      -- type vocabulary + environment
│   ├── StateMachine.hs       -- graph extraction, reachability, deadlocks
│   └── Emit.hs               -- deterministic JSON report
├── test/                     -- HSpec suites + golden tests
├── examples/                 -- escrow, voting, token_sale, deadlock
├── flake.nix                 -- reproducible build & dev shell
└── covenant.cabal

---

Testing

cabal test all --test-show-details=direct

50 tests across five suites, including golden tests that pin the JSON report byte-for-byte (test/golden/*.expected.json). To regenerate a golden file after an intentional format change:

cabal run covenant -- verify --format json test/golden/escrow.cov > test/golden/escrow.expected.json

---

Design highlights

• Scannerless parsing — the parser runs directly over Text with Megaparsec's lexeme combinators, sharing one source of truth for whitespace and word boundaries instead of materialising a separate token stream.
• Monad-transformer stack, chosen per phase — the type checker writes its environment in a StateT pass and only reads it in a ReaderT pass, so the type itself documents each phase's capability.
• Plain ADTs over GADTs — the surface AST stays simple; the invariants that matter here (reachability, name resolution) are environment/graph properties, not type-level ones.
• Deterministic output — sorted keys and normalised lists make the JSON report stable enough to golden-test, and colour is emitted only to an interactive terminal.

---

License

BSD-3-Clause © 2026 Gabriel.