C Note
black_scholes_call
European call, closed form
intrinsic_value proven
lower_bound_disc breaks
- 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
Verified quantitative computing
Provable, not plausible.
The verified runtime for AI-generated quantitative code. Writing and proving happen together, so what the agent produces arrives with evidence bound to it. When a property breaks, the input that broke it is caught before production, not discovered in it.
The problem
The review gap
The dangerous error in quantitative code is silent: a wrong Greek, a sign flipped in a hedge, a curve that dips negative where it never should. Nothing crashes. The number looks like every other number, and it reaches production unread. Coding agents produce more of this code in a day than a careful reviewer reads in a week.
Formal methods waited decades for a workflow worth their cost. Code written by machines and supervised by people is that workflow.
What you open
The C Note
C Proof changes what the agent hands you. Instead of source code plus a request for trust, each model arrives with a record of what was checked, what held, what broke, and the input that broke it. Review starts from evidence, not from a blank diff.
The C Note is the page a reviewer opens. Every line names its evidence: an SMT proof under declared domain assumptions, or property validation with its preconditions and sample count. Validation is labeled validation, never relabeled as proof.
C Note
black_scholes_call
European call, closed form
Properties checked for this model
- intrinsic_value intrinsic(S, K) >= 0proven
- df_bounded 0 < df <= 1sampled, not proven
- upper_bound C <= Ssampled, not proven
- put_call_parity C - P == S - K * dfsampled, not proven
- vol_monotone sigma2 >= sigma1 implies C(sigma2) >= C(sigma1)sampled, not proven
- delta_range 0 <= dC/dS <= 1sampled, not proven
- vega_sign dC/dsigma >= 0sampled, not proven
- gamma_sign d2C/dS2 >= 0sampled, not proven
- lower_bound_disc C >= max(S - K * df, 0)disproved
sampled rows: 10,000 samples per property, seed recorded
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.
A hold cites its proof. A break names its witness. Nothing is summarized into a checkmark.
Built on Chelis
The trust stack
What makes a C Note worth reading is what stands under it. Chelis is the statically typed substrate underneath C Proof; the trust stack is four layers from a mechanized foundation to an audit chain a reviewer can walk end to end.
-
Foundation
Lean 4 mechanized soundness of the language semantics. Type-system guarantees rest on machine-checked theorems.
-
Static edge
The compiler refuses structural bugs that survive review in Python. If it contradicts the declared program, it does not compile.
-
Property verification
The C Proof Engine routes each property to the strongest proof available. Type-level discharge where structural, SMT where algebraic, certified-envelope verification where the engine achieves coverage over transcendental paths. Properties beyond solver and envelope reach run as labeled validation.
-
Audit chain
Every property carries its tier, evidence, solver, and provenance from source spec to compiled binary.
Work enters as LaTeX with provenance, typed Python migrated at the boundary function by function, requirements written as executable properties, or native Chelis.
First application
Finance first
The first application is the options and derivatives desk, where a wrong number is priced the same day. Pricing kernels, Greeks, curves, and risk aggregation run as checked programs against a canon of what must be true for an options model.
- Greeks and pricing kernels
- Yield curves and stochastic processes
- Risk measures and portfolio constraints
- Signals, optimization, and linear algebra
Deployment
Controlled boundary
Your models, positions, and build paths never leave your environment. C Proof runs where they already live.
- Runs on infrastructure you control
- No hosted dependency for proprietary models or positions
- Compiler source visible under enterprise agreement
- No public registry in the build path
Teams
Who owns this
Quant research and trading leads
You own the pricing, signal, and risk code that agents now write. C Proof gives each generated kernel a checked path to the desk and a C Note you can read before the code trades.
Model risk and validation
You sign off. The C Note carries the property list, what held and what broke, the witnessing inputs, and provenance from the approved specification to the compiled binary, in one reviewable chain.
Engineering leadership
You set the path generated code takes into production. C Proof narrows that path to one where structural errors fail the build instead of surfacing downstream.
Security and compliance
You control what enters the environment. Source visibility under enterprise agreement, no public registry in the build path, deployment inside infrastructure you run.
Next step
Talk to us
Bring a pricing or risk kernel your desk already runs. We will map the properties it must satisfy, the evidence each one gets, and what its C Note would show.