How it works

From model to C Note

C Proof starts from the artifact your team already trusts, a formula, a typed Python function, an approved requirement, or native Chelis, and ends at a checked binary with a C Note attached. Along the way the compiler and the property layer decide what is proved, what is validated, and what is refused.

Input
Chelis
Type system
Properties
C Note

Chelis

Checked substrate

In plain terms: mistakes Python raises at runtime, or never raises at all, do not compile here.

Chelis is a statically typed functional language built for numerical code that agents can generate faster than humans can review. It gives C Proof a boundary Python does not: the compiler can reason about the parts of a quantitative implementation that usually stay implicit.

Dimensions

Tensor axes carry semantic names. A book exposure cannot be silently added to a hedge vector with a different axis.

Precision

Numeric precision is explicit in the type. An f32 path mixing with f64 data is visible at build time.

Effects

Randomness, I/O, and accumulation are tracked as effects instead of hidden inside ordinary function calls.

Linearity

Resources that must not be duplicated or dropped are enforced by the compiler boundary.

Derivatives

Supported differentiable paths tie sensitivities back to the function being differentiated, rather than to a side calculation.

Inputs

Approved sources

In plain terms: you do not rewrite your stack. A formula, a typed Python function, or an approved requirement enters one at a time, and each keeps a pointer back to where it came from.

Start from the artifact that already carries intent. Math and requirements keep provenance into Chelis, so a proof artifact can point back to the source formula or requirement that produced it.

LaTeX model

Math spec

Start from a model a quant team already reviews. C Proof preserves source spans while lowering the formula into typed Chelis.

Source model

C = S N(d_1) - K e^{-rT} N(d_2)

Chelis + provenance

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)
}

Typed Python

Migrated kernel

Move numerical code function by function. Typed boundaries expose shape and precision gaps before surrounding Python has to move.

Python

def predict(x, w, b):
    return x @ w + b

Chelis

def predict(
  x: tensor[64, 64, f32],
  w: tensor[64, 1, f32],
  b: tensor[1, f32]
) -> tensor[64, 1, f32] =
  x |> matmul(w) |> add(expand(b, 0, 64))

Structured requirement

Requirement property

Turn approved structured English into an executable property bound to the function it constrains.

Requirement

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

@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.0

Chelis-native

Native model

Write directly in Chelis for new or sensitive kernels and keep the same proof and build path.

Chelis

def score_path[scenario](
  exposure: &tensor[scenario, f32]
) -> tensor[scenario, f32] =
  exposure |> relu |> sigmoid

Checked artifact checked binary, C Note, emitted code

Verification

Specification match

In plain terms: the type system refuses structural mistakes, and properties check the implementation against what the specification says it must do.

The type system rejects structural numerical errors first. The property layer checks whether the implementation satisfies the approved specification that came from math or requirements. The detailed proof tiers live on the proofs page.

Type boundary

The compiler rejects structural errors before a binary is produced.

def combine_exposure[book, hedge](
  exposure: tensor[book, f32],
  offset: tensor[hedge, f32],
) -> tensor[book, f32] =
  exposure |> add(offset)

Here the return promises the book axis, while the offset carries a different hedge axis.

Property boundary

Properties state behavior the implementation must satisfy. They are discharged by proof where possible and kept explicit as validation evidence when proof is not the right route.

@property prop_FIN_002 forall(P: f32, S: f32, K: f32, r: f32, t: f32)
  where t > 0.0, r >= 0.0:
  {
    parity_call = P + S - K * exp(0.0 - r * t)
    put_call_parity_residual(parity_call, P, S, K, r, t) == 0.0
  }

The property states the residual that must reduce to zero under the stated preconditions.

Output

The C Note

What comes out is a checked binary and the C Note that goes with it. For every property the C Note records the route (type system, SMT, or validation), the assumptions in force, and the outcome. A property that holds cites its evidence. A property that breaks names the input that broke it. Provenance runs back to the formula span or requirement line that produced the property.

Pipeline from source artifact to Chelis, checked intermediate representation, proof artifacts, and emitted target code — Source spec, checked Chelis, C Note, emitted C, HIP, or Metal.

The change view of the same worked example: a fix lands, the broken property re-checks, and the evidence is re-recorded.

C Note

black_scholes_call

European call, closed form

model: black_scholes_call
source: LaTeX model, lowered to Chelis
domain: S > 0, K > 0, T in (0, 2], sigma in [0.05, 0.60], r in [0, 0.10]

lower_bound_disc 1 counterexample

S: 150.00
K: 50.00
r: 0.02
sigma: 0.15
T: 0.25

model C: 100.2394
bound: 100.2494
shortfall: -0.0100

The rational CDF approximation saturates near 1 in the upper tail.

-def normal_cdf(x: f32) -> f32 = rational_cdf_tail(x)

+def normal_cdf(x: f32) -> f32 = 0.5 * (1.0 + erf(x / sqrt(2.0)))

lower_bound_disc

sampled, not proven on the declared domain

The other properties hold unchanged, evidence re-recorded.

artifact: proof and validation record · provenance to source formula

A worked example: a call priced deep in the money to exhibit the saturation regime, with the values shown exactly as a C Note records them.