An agent turns your request into Chelis code. The compiler rejects mistakes in shapes and dimensions before anything runs. The C Proof Engine then checks each property you state: it proves it, tests it on samples when no proof applies, or returns the input that breaks it.
We created Chelis, the verified tensor language for agent-written code, and publish it under MIT on GitHub. The compiler rejects each of these, whether a person or an agent wrote the code:
| Check | Rule | What it catches |
|---|---|---|
| Shapes | Nothing stretches to fit. A change of rank is written out. | A vector broadcast against a matrix into the wrong shape. |
| Named dimensions | Dimensions match by name: book never matches hedge. | Two axes of the same length swapped or added together. |
| Precision | One precision per operation; cast converts. | f32 quietly mixed into f64 data. |
| Effects | A function's type lists its effects. A random draw takes an explicit key. | Random draws that cannot be replayed. |
| Ownership | Each tensor has one owner; & borrows it read-only. | A slice that rewrites its parent array. |
The Chelis tour shows each rule with the code it rejects, and chelis.ch/research covers the design.
The agent writes code from your request, a formula from a paper, a requirement in structured English or typed Python, and you can write Chelis directly. Formulas and requirements keep their provenance, so every result links back to its source line.
A pricing formula is translated into typed Chelis, and each line links to its span in the source.
C = S N(d1) - K e-rT N(d2)
def call_price(
spot: f32, strike: f32, rate: f32, sigma: f32, tenor: f32
) -> f32 = {
d_1 = d1(spot, strike, rate, sigma, tenor)
d_2 = d2(spot, strike, rate, sigma, tenor)
discount = rate |> mul(tenor) |> neg |> exp
spot_leg = spot |> mul(normal_cdf(d_1))
strike_leg = strike |> mul(discount) |> mul(normal_cdf(d_2))
sub(spot_leg, strike_leg)
}A requirement in structured English becomes a property, bound to the function it constrains.
FIN-001 for call_price :: (S: f32, K: f32, r: f32, sigma: f32, t: f32) -> f32
WHEN K > 0.0 AND t > 0.0
the system shall return a non-negative call price@property prop_FIN_001 forall(S: f32, K: f32, r: f32, sigma: f32, t: f32)
where K > 0.0, t > 0.0:
call_price(S, K, r, sigma, t) >= 0.0Port numerical functions one at a time; their shapes and precision go into the Chelis signature.
New kernels are written in Chelis and get the same checks.
Two kinds of check run in order: the type check on the whole program, then each property you stated. The proof methods are explained on Proofs.
The return type is indexed by the book dimension, but the offset is indexed by the hedge dimension.
Type check
$ chelis check combine_exposure.chdef combine_exposure[book, hedge](exposure: tensor[book, f32], offset: tensor[hedge, f32]) -> tensor[book, f32] = exposure |> add(offset)DimensionMismatchdistinct declared dim parameters `book` and `hedge` were unified by the function body in declaration `combine_exposure`: authored dimension binders are rigid and must remain distinct (spec/04-type-system.md §3.1.3 [04-INF-6])For any positive rate, the discount factor lies strictly between zero and one. C Note proves this over the real numbers.
def discount_factor(r: f32) -> f32 = (1.0 / (1.0 + r))
@property df_bounded forall(r: f32) where r > 0.0:
((discount_factor(r) > 0.0) && (discount_factor(r) < 1.0))Proven (SMT)
df_bounded
Method: SMT proof over the real numbers, not 32-bit floats.
Goal:
forall(r: f32) where r > 0.0: ((discount_factor(r) > 0.0) && (discount_factor(r) < 1.0))
A property the SMT solver proves over the reals, with no sampling.
For each property: the method (SMT proof, SMT with a certified envelope, or sampled validation), the assumptions and the result. A disproved property carries its counterexample, and every result links back to its source.
Sampled, not proven
bs_call_positive
Method: sampling
Goal:
forall(s: f32, k: f32, r: f32, sigma: f32, t: f32) where s > 0.0, k > 0.0, sigma > 0.0, t > 0.0, r >= 0.0: (bs_call(s, k, r, sigma, t) > 0.0)
Validated by sampling only, not an SMT proof.
Open a checked example in C Note, or send us a property from your own code.