Today we're releasing Chelis, a programming language for numerical code written by AI coding agents. The compiler, the standard library and a set of domain libraries are on GitHub under the MIT license.
Most of the code I ship these days, I didn't type. An agent wrote it and I read it. For a lot of software that works fine. For numerical code it works much less well, because a wrong answer looks exactly like a right one. A transposed matrix is still a matrix. A probability that drifts to 1.03 still prints as a number. Review catches some of this, on a good day. We wanted a language that catches it before review starts.
What Chelis is
Chelis is a statically typed functional language with tensors built into the type system. You write a program, the compiler checks it, and chelis build compiles it into a native executable. Here is the first program from the docs:
def relu_then_softmax[n](x: tensor[n, f32]) -> tensor[n, f32] = x |> relu |> softmax(0)result = [-1.0, 0.0, 1.0] |> to_tensor(f32) |> relu_then_softmaxThe n is a dimension variable. This function takes a vector of any length, and its signature says it hands back a vector of that same length with f32 elements. Shape and precision are part of the type, and the checker holds every caller to them.
chelis fmt --inplace app.chchelis check app.chchelis eval --file app.chchelis build app.ch --output out/Why a new language
Agents are good at producing code that looks plausible. In Python, the feedback an agent gets on a shape bug is a stack trace halfway through a run, or nothing at all. So the agent guesses, and you inherit the guess.
We designed Chelis around the loop an agent actually runs: write some code, check it, read what the compiler says, fix it, go again.
Tensor shapes and element types live in the type system, so dimension mismatches are compile errors. Effects are tracked in types too, and randomness takes explicit keys, so a function's signature tells you whether it can touch the outside world and makes sampled code reproducible. Automatic differentiation and vectorization come as language-level transforms, grad and vmap, and the checker understands both. The syntax is meant to be read by a human supervising the work.
Under all of that sits soundness. When the checker accepts a program, the types hold.
Built for agents
Chelis treats the agent as the primary user of the compiler. chelis tide mcp starts an MCP server that gives your agent tools to check, evaluate, prove and structurally edit code directly, with no shell scraping involved. The commands report in JSON, exit codes carry meaning, and chelis prove --capabilities tells an agent what this particular build can do before it asks for anything. Diagnostics are written for an agent to act on. When code reaches into a type it isn't allowed to construct, the error names the type, the module that owns it, and the exported functions that produce it. The formatter gives every program one canonical form, which keeps agent diffs small and readable.
To bring an agent up to speed, point it at our skill file at chelis.ch/SKILL.md, or paste a single line into a session: Read https://chelis.ch/SKILL.md and use it when writing Chelis. There is also an llms.txt that lists the pages an agent should read first.
Proving properties
Types catch shape and precision mistakes. For other claims, you state what should be true as a property, and chelis prove checks it:
@property nonnegative forall(x: f32): ((x * x) >= 0.0)The prover works in tiers. It can check a goal with the type system, try induction, hand the goal to an SMT solver, or sample inputs. The default auto tier tries them in that order: induction when a property calls a recursive function, otherwise the solver, then sampling. Every result reports which method produced it, along with a verdict that states exactly what was established. A sampled pass comes back as fuzz_validated. A solver proof over real arithmetic comes back as proven_modulo_real_arithmetic. An agent, or a reviewer, can read that and know what kind of yes it is.
Opaque types with declared invariants bring this to application code. Here is a probability type that has to stay in the unit interval:
@opaque@invariant(p) ((p.value >= 0.0) && (p.value <= 1.0))type Probability = | Probability { value: f32 }Other modules can use a Probability, but they can't forge one. Every exported function that returns a Probability becomes a proof obligation: it has to show its output satisfies the invariant. Drop the upper bound check from a constructor and the prover hands back a counterexample. That is the bug an agent would otherwise have shipped, caught before anyone read the diff.
Numerical libraries
Chelis targets numerical computing and the fields built on it. Nautilus covers scientific computing: special functions, probability distributions, linear algebra, statistics, and solvers for roots, ODEs, SDEs, integration and optimization. Coral is a dataframe library for the joins, group-bys and rolling windows that every analysis eventually needs. Shoals is for quantitative finance, with option pricing, Greeks through automatic differentiation, volatility surfaces, yield curves, day counts, XVA, and money values tagged with their currency. Economoist covers quantitative economics, including Markov transitions, Bellman operators and present value models.
Shoals and Economoist both ship property specifications and worked counterexamples, so you can see the prover catching realistic mistakes in pricing and modeling code.
Getting started
The release supports Apple silicon Macs (arm64) and x86_64 Linux. It runs on the CPU, so you don't need a GPU. You install it with chelisup, the Chelis toolchain manager, and Get started walks through each step. From there, the fastest route is to give your agent the skill file and ask it to write something you understand well, then watch the loop run. If you'd rather learn the language yourself, the hello-chelis guide is a curriculum that runs from a first tensor through capstone examples.
What's in this release
The core language and the CPU backend, which compiles programs to native executables, are the center of this release.
GPU acceleration is experimental. Chelis has HIP and Metal backends for AMD and Apple GPUs, selected with chelis build --target hip or --target metal. They are still under active development, so expect rough edges and use the CPU backend for work you depend on.
The domain libraries are alpha. They are useful today, and their APIs will move as we learn from people using them.
Open source
Chelis is MIT licensed. The code and the issue tracker are public, and we'd love bug reports, feature requests and questions. We aren't accepting outside contributions at this time.
Chelis is released by C Proof, and it's the language underneath C Note, our verified computing notebook.
Where this goes
I spent years working on PyTorch, a framework built around a dev at a keyboard writing a model by hand. That dev is still at the keyboard. More and more, though, their job is reading what an agent wrote and deciding whether to trust it. The hard part of programming is shifting from getting the computer to do what you meant toward knowing that it did.
Agents will keep getting better at writing code. How much we can build on their work depends on how much of it we can trust without rereading every line. Trust comes from tools that hand back evidence along with the program: types that know the shape of your data, sound formal proofs, and counterexamples you can rerun.
Chelis is our attempt at that kind of tool, starting with the numerical code where mistakes are expensive. We've learned the most about it by watching agents write it, and we're looking forward to seeing what yours make.
The Chelis core team is Jeff Smith, Robert Ronan, Britton Robitzsch, and Gerasimos Lampouras. Prior core team members include Vivek Kondapalli.