Research
How chelis prove checks the properties you state about your code, and the core calculus of Chelis in Lean 4.
How chelis prove checks a property
A property is a Chelis function that states something about your code. chelis prove finds the properties in a package and checks each one with these methods:
- Type checking
- A property that is not well typed is rejected before any solver runs.
- SMT solving
- cvc5 proves algebraic and polynomial properties over the reals.
- Certified envelopes
- Each call to
erf,exp,logorsqrtbecomes a variable held inside a certified bound on that function, and cvc5 proves what remains. - Bound propagation
- Intervals and zonotopes pushed through the compiled graph bound the range of a scalar output.
- Seeded sampling
- Other properties run on seeded samples, so every result can be reproduced.
LaCaDiLE
A first-order core calculus of Chelis in Lean 4, covering tensor derivatives, logical ownership, keyed randomness and resource protocols.
The type system reference states the rules the checker enforces.