Skip to content
Chelis docs

Getting started

Install

Section titled “Install”

Economoist is distributed as a reef package. Install it from the Chelis-Lang GitHub org:

Terminal window
chelis reef install --from-github Chelis-Lang/economoist@v0.2.3

This pins to chelis 0.14.0. If your local toolchain is older, update chelis first.

Build

Section titled “Build”

Compile the models:

Terminal window
chelis reef build

This type-checks all Economoist modules and produces the intermediate representation consumed by the prover.

Prove

Section titled “Prove”

SMT proving ships in chelis v0.11.0 and later. To discharge every property in the package:

Terminal window
chelis prove

The prover delegates to cvc5 over the theory of reals. Each property either receives an unqualified green (proven) or reports a counterexample. There is no intermediate "maybe" state.

Gate

Section titled “Gate”

To enforce that all properties remain green in CI or local pre-commit:

Terminal window
python3 scripts/prove_gate.py

The gate script exits non-zero if any property fails to discharge. It produces a structured JSON report suitable for CI artifact upload.