Chelis

Shells

One ecosystem, one tensor graph

Shells are reef packages that ride the Chelis runtime. Numeric work composes with the compiler's tensor graph instead of sitting beside it, so automatic differentiation flows through every one of them.

Core runtime

The runtime that ships in the compiler

Every shell rides the same tensor DAG, so automatic differentiation flows through all of them.

chelis-std glyph

chelis-std

The compiler-bundled runtime: the elementwise ops and reductions every other shell builds on, shipped inside the compiler.

Read the docs →

Numerical and data

Numbers and tables, typed end to end

nautilus glyph

nautilus

Numerical methods, statistics, and optimization in pure Chelis, with automatic differentiation flowing through every function.

Read the docs → coral glyph

coral

Typed dataframes whose columns are tensors, so a table pipeline composes with the tensor DAG instead of sitting beside it.

Read the docs →

Machine learning

Models on a checkable substrate

school glyph

school

A deep-learning framework on Chelis: compose architectures from typed layers, differentiate them with the language's grad, and train with real optimizers and training loops, all on the tensor graph the compiler checks.

Read the docs →

Bridges

Bring code in from where it already lives

octant glyph

octant

LaTeX-to-Chelis translation that tracks provenance, so a compiled trace points back to the original formula.

Read the docs → calcify glyph

calcify

Python-to-Chelis translation, carrying numeric code onto the typed tensor graph.

Read the docs → hydronnx glyph

hydronnx

The ONNX shell, reading exported models into Chelis Deep.

Read the docs → c-earchin glyph

c-earchin

Structured English requirements (EARS) translated into executable Chelis properties, with provenance from each requirement line to its witness.

Read the docs →

Domain shells

Built for the fields that need the proof

shoals glyph

shoals

Quantitative finance on typed tensors: pricing, risk, curves, and stochastic processes, with derivatives the compiler differentiates for you.

Read the docs → whale glyph

whale

A reusable betting shell for sizing stakes from odds and edges, with Kelly variants and bankroll discipline on the same checked substrate.

Read the docs →

Verification

The language checked against itself

beacon glyph

beacon

Bound-propagation verification over compiled Chelis programs: proves output-range properties over real arithmetic by flowing interval and zonotope bounds through the DAG, with optional Arb-backed enclosures.

Read the docs → economoist glyph

economoist

Verified economic and dynamic-programming models: structural properties are proven at the SMT tier over the reals by cvc5, with sensitivity analyses validated by seeded sampling.

Read the docs → hull glyph

hull

A Chelis-language reference implementation of the type checker and evaluator, run alongside the compiler on generated programs to catch drift between the proved language and what ships.

Read the docs →

Learning

Start here

hello-chelis glyph

hello-chelis

A complete, runnable example project covering the language and every official shell, with a guided curriculum from first tensor to end-to-end ML pipeline.

Read the docs →