Economoist
Economoist is the Chelis shell for verified economic and dynamic-programming models. It ships as a reef package (v0.2.3, pinned to chelis 0.14.0) and provides a catalog of structural economic properties, each discharged by cvc5 over the mathematical reals.
The SMT-green guarantee
Section titled “The SMT-green guarantee”Every property in Economoist carries an unqualified SMT green. This means:
- The property is proven at the SMT tier by cvc5, working over the theory of reals.
- There is no fuzz sampling. No contract annotation standing in for a proof. The solver either discharges the property or it does not.
- A green is a genuine theorem of the model at the stated dimension, not a probabilistic assertion.
Economoist covers economic primitives: Markov transition operators, Bellman operators, growth models, present-value identities. Finance and derivatives (pricing, hedging, Greeks) are handled by a separate shell. The boundary is clean: if the object is an economic model or a dynamic-programming recursion, it belongs in Economoist. If it prices a traded instrument, it belongs elsewhere.
Relationship to the broader verification story
Section titled “Relationship to the broader verification story”Chelis provides a layered verification architecture. Economoist uses the SMT tier (cvc5 over the reals) because the economic properties it targets are quantifier-free or existentially quantified statements about finite-dimensional linear and nonlinear operators. This tier is fully automatic: you write the model, state the property, and run chelis prove. No manual proof script is required.
The structural greens Economoist provides are fixed-dimension instances (n=2, n=3). Convergence theorems and general-n results require induction and sit outside the SMT tier. See Boundaries for what is and is not covered.