How it works

From model to C Note

C Note is the surface where you author and inspect a model. Chelis type-checks each property first; the C Proof Engine then dispatches proof-eligible goals and labels validation when no proof route closes.

Surface

C Note

Write a model, run it, and inspect what was proved, validated, or broken.

Proof engine

Type-checks first, then dispatches each property

Gate · Type system
Prove · SMT + certified bounds
Fallback · Labeled validation

Certified envelopes bound supported transcendental subterms; SMT proves the residual. When no proof closes, validation stays labeled.

Foundation

Chelis

Its type system rejects structural mistakes; Lean 4 mechanization backs the language rules.

Chelis

Checked substrate

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: structural mistakes that Python raises at runtime, or never raises at all, do not compile here.

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 C Note, start with the assistant, a blank notebook, or a formula imported from a paper. At the system boundary, a formula or approved requirement enters one at a time and keeps provenance into Chelis, so an evidence artifact can point back to the source 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)
}

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

Typed Python

Move numerical functions at the boundary. Their declared shapes and precision become explicit before surrounding Python has to move.

Native Chelis

Write new or sensitive kernels directly in the checked language and keep the same evidence path.

Verification

Specification match

The type system refuses structural mistakes first. Properties then check the implementation against the approved specification that came from math or requirements. The detailed evidence routes 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 evidence: type-system discharge; an SMT result with any certified-envelope bound and qualifier; or labeled validation. It also records 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 source that produced the property.

This panel names the method, assumptions, and result. Here an SMT solver discharges the property over the real numbers, with no sampling and no contract, and cites the code it references.

A C Note verdict panel reading Proven (SMT): the method is an SMT proof over the reals with no sampling and no contract, followed by its hypotheses, goal, and referenced function.

Get started

Try a checked model

Open a checked example in C Note, or bring a property your review currently takes on trust.

Try C Note Talk to us