Chelis is a numerical computing language for code that agents write and people supervise. Tensors carry named dimensions and precision in their type, and a proof stack checks the properties you state.
def portfolio_return(w: tensor[3, f64], r: tensor[3, 1, f64]) -> tensor[f64] = {
weighted = mul(w, r)
weighted |> sum(0)
}
In numpy, returns shaped 3 by 1 stretch against three weights into a 3 by 3 grid and
the sum comes back as a plausible wrong number. chelis check rejects the same
multiply before anything runs. The error from its JSON report:
{"kind":"DimensionMismatch","message":"`mul` argument 2: expected rank-1 tensor, got rank-2 tensor","severity":0.8,"expected":"rank-1 tensor","got":"rank-2 tensor","span":{"span":"point","offset":94},"span_id":"surf:94..103"}- Checked before it runs. The compiler checks shapes, precision, effects, and
ownership. Dimensions match by name,
f32andf64do not mix without acast, I/O appears in a function's effects, and random operations take explicit keys. - An agent in the loop.
chelis checkanswers in JSON with the error kind and source span, and the same input always gets the same answer.chelis tide mcpgives an agent check, eval, prove, and structural edits as MCP tools. - Properties you can review.
chelis provechecks@propertydeclarations with type checking, an SMT solver, or seeded sampling, and each result names the method behind it. A second checker written in Chelis cross-checks the compiler, and a core calculus of Chelis is mechanized in Lean 4. - General-purpose numerics. Surf (
.ch) is the readable syntax; Deep (.dp) is the canonical form the compiler and agents use. Programs build to C. Shells, installed with Reef, cover numerical methods (Nautilus), dataframes (Coral), and quantitative finance (Shoals).
Install
Chelis is distributed as prebuilt binaries for Linux x86_64 and macOS arm64,
published on the releases
page. The install guide has the
steps and the native C compiler chelis build needs on each platform.
Documentation
The Chelis guide covers the first program,
the CLI, types, effects, properties, and Reef packages. The same guide is the
mdBook in docs/book, rendered from chelis.ch; build it locally
with mdbook build docs/book. The examples directory holds executable
Chelis programs.
License
MIT