The verified tensor language for agent-written code.
Chelis checks tensor shapes and precision before the code runs, and a bad index stops the program, so an agent's mistake becomes an error instead of a wrong number.
chelis 0.19.1 · Linux x86_64 · macOS arm64 · MIT
Catch the wrong number in the loop, not in production
No person waits on the agent's loop and nothing reaches production. Chelis checks shapes, precision, effects and ownership there, before the code runs.
Automatic cheap: no person waits, nothing reaches production
People and production expensive: a person's time, numbers others use
Python today
-
Write: The agent writes numpy.
-
Check: Tests pass.
-
Fix: Looks done.
-
Prove: Waits for review.
-
Review: A person reads every line.
-
Deploy: It ships.
-
Production: Reports 0.060, not 0.023.
wrong number
Chelis
-
Write: The agent writes Chelis.
-
Check:
rejectedchelis checkrejects the multiply: a JSON diagnostic. -
Fix: The agent repairs until no errors remain.
-
Prove:
chelis provechecks the stated properties. -
Review: A person reads types and properties.
-
Deploy: Code that checks ships.
-
Production: Runs the checked code.
Shapes, precision, keys, and ownership
Pick a rule to see a program and its compiler or runtime result.
Shapes
numpy 0.060 instead of 0.023, with no warning
Chelis stops at mul(w, r) before anything runs
broadcast.ch
def portfolio_return(w: tensor[3, f64], r: tensor[3, 1, f64]) -> tensor[f64] = {
weighted = mul(w, r)
weighted |> sum(0)
}chelis check broadcast.ch
DimensionMismatch: `mul` argument 2: expected rank-1 tensor, got rank-2 tensor --> broadcast.ch:2:14
| 2 | weighted = mul(w, r) | ^^^^^^^^^
The returns arrive shaped 3 by 1, and numpy stretches them against the three weights into a 3 by 3 grid before the sum.
Named dimensions
jaxtyping accepts a (seq, batch) array as (batch, seq) when both are 128
Chelis rejects the call: seq is not batch
axes.ch
def score(x: tensor[batch, seq, f32]) -> tensor[batch, seq, f32] = relu(x)
def caller(y: tensor[seq, batch, f32]) -> tensor[batch, seq, f32] = score(y)chelis check axes.ch
DimensionMismatch: `score` argument 1, axis 0: expected batch, got seq --> axes.ch:2:69
| 2 | def caller(y: tensor[seq, batch, f32]) -> tensor[batch, seq, f32] = score(y) | ^^^^^^^^
| 2 | ...tensor[batch, seq, f32] = score(y) | ^^^^^^^^
batch and seq stay distinct even when both are 128. permute puts them in order.
Precision
numpy adds f32 to f64 and quietly returns f64
Chelis rejects the add, and the report suggests cast
precision.ch
def add_mixed(a: tensor[3, f32], b: tensor[3, f64]) -> tensor[3, f64] = add(a, b)chelis check precision.ch
PrecisionMismatch: `add` arguments; tensor precision mismatch: f32 vs f64 --> precision.ch:1:73
| 1 | def add_mixed(a: tensor[3, f32], b: tensor[3, f64]) -> tensor[3, f64] = add(a, b) | ^^^^^^^^^
| 1 | ...f64]) -> tensor[3, f64] = add(a, b) | ^^^^^^^^^
= suggestion: Insert explicit cast f32 and f64 meet only through cast, and the report suggests it.
Randomness
numpy draws from hidden global state
Chelis rejects a draw that has no key
randomness.ch
def shock(px: tensor[3, f32]) -> tensor[3, f32] = {
noise = uniform_like(px, -0.5f32, 0.5f32)
add(px, noise)
}chelis check randomness.ch
ArityMismatch: call `uniform_like`: expected 4 arguments, got 3 arguments; `uniform_like(t, low, high)` is the retired counter-stream spelling: a random draw takes an explicit key first, `uniform_like(k, t, low, high)` (spec/05-risc-primitives.md section 2.7) --> randomness.ch:2:11
| 2 | noise = uniform_like(px, -0.5f32, 0.5f32) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
= suggestion: Pass a key first: make one with `key_from_seed(seed)` and derive more with `split_key`, `split_keys` or `fold_in`, as in `uniform_like(k, t, low, high)` The checker rejects a draw without a key. key_from_seed(7i64) supplies one for a repeatable draw.
Ownership
numpy changes the parent array through a slice
Chelis rejects a borrow passed to an owned parameter
aliasing.ch
def update(x: tensor[3, f32]) -> tensor[3, f32] = relu(x)
def reader(x: &tensor[3, f32]) -> tensor[3, f32] = update(x)chelis check aliasing.ch
TypeMismatch: type mismatch: tensor[3, f32] vs &tensor[3, f32] --> aliasing.ch:2:52
| 2 | def reader(x: &tensor[3, f32]) -> tensor[3, f32] = update(x) | ^^^^^^^^^
| 2 | ...f32]) -> tensor[3, f32] = update(x) | ^^^^^^^^^
The NumPy slice shares storage. The Chelis snippet checks an ownership boundary: reader must use copy(x) to pass its borrow to update's owned parameter.
Indexing
Python reads px[-1], the last price
Chelis stops the program at the read
negative_index.ch
def previous(px: List[f64], i: i64) -> f64 = index(px, (i - 2i64))
def main() -> f64 = previous([101.0f64, 102.5f64, 99.0f64], 1i64)chelis eval --file negative_index.ch
error: index requires non-negative index, got -1
A negative index stops the program instead of reading from the end of the series.
Keep going
chelis prove with cvc5, and a first-order core calculus in Lean 4 Shells nautilus, coral, shoals, economoist Docs The Chelis, coral and nautilus books MCP tools chelis tide mcp: check, run, prove and edit tools for an agent Agent skill SKILL.md for your coding agent Install Chelis 0.19.1
Chelis installs with chelisup, its toolchain manager. A short script on each release puts chelisup in ~/.chelis/bin; chelisup then downloads the compiler for Linux x86_64 or macOS arm64 and keeps versions side by side. chelis build compiles a program to native code.
# Get the installer script from the latest release $ gh release download -R Chelis-Lang/chelis -p chelisup.sh # Install chelisup into ~/.chelis/bin and put it on your PATH $ sh chelisup.sh $ export PATH="$HOME/.chelis/bin:$PATH" # Install the compiler $ chelisup install 0.19.1