How it works
Three ways in, one substrate you can audit.
Code that matters arrives in three forms: as mathematics on the page, as a requirement someone signed off on, and as the codebase a team already runs. C Proof takes each one onto the same verified substrate, with an audit chain that runs from the source your team approved to the binary that executes.
Path 1: from the math
A formula on the page becomes a binary you can trace back.
1. The formula stays the source of truth
Octant is a LaTeX-to-Chelis bridge with provenance. It translates a subset of mathematical LaTeX into Chelis Deep s-expressions and attaches span information to every emitted node. The formula your team approved and the code that runs are the same artifact, with a recorded link between them.
The Black-Scholes call price, as it is written in a textbook:
c = s \Phi(d_1) - k e^{-r t} \Phi(d_2)Octant checks its translations against a corpus of textbook formulas cited to their sources, paired with canonical Chelis forms held as an equivalence oracle, so a translation that drifts from the published math is caught rather than trusted.
2. Deep is what the compiler reads
Chelis has two syntaxes. Surf is the readable form for humans. Deep is the canonical s-expression form for machines and the compiler, and Surf desugars to Deep with a lossless round-trip. Octant emits Deep directly, so the generated artifact is the one the compiler will check, not a translation of it.
The call price as Octant emits it, in Chelis source:
import Nautilus.Special (normal_cdf)
def c(s: f32, k: f32, r: f32, t: f32, d_1: f32, d_2: f32, e: f32) -> f32 = sub(mul(s, normal_cdf(d_1)), mul(mul(k, exp(mul(log(e), mul(sub(0, r), t)))), normal_cdf(d_2)))The helper terms factor out the same way the textbook does, as their own definitions:
def d(s: f32, k: f32, r: f32, t: f32, sigma: f32) -> f32 = div(add(log(div(s, k)), mul(add(r, div(mul(sigma, sigma), 2)), t)), mul(sigma, sqrt(t)))
def d(d_1: f32, sigma: f32, t: f32) -> f32 = sub(d_1, mul(sigma, sqrt(t)))3. The same checks as hand-written Chelis
Octant output goes through the verification chain that any Chelis program does: type checking, effect and linearity validation, lowering to RISC IR, code generation, and property fuzzing. There is no separate, weaker path for generated code. The type system tracks named tensor dimensions, numeric precision, differentiability, and ownership at compile time, so a shape mismatch or a precision error is a build failure, not a run-time surprise.
4. One binary, one target flag
Chelis compiles to a single binary with the backend chosen at build time by a target flag. The C backend (with OpenMP and BLAS) is the default; the HIP and Metal backends are selected by the same flag. The numerical surface comes from the standard library, so the same source compiles to whatever target your infrastructure expects.
5. A binary you can trace back
The audit chain runs end to end: a LaTeX byte range maps to a Deep node, which maps to an IR or HostExpr node, which maps to a line of emitted C, HIP, or Metal source. When a number comes out wrong, you can walk it back to the character in the formula that produced it. That is the property that makes generated code reviewable instead of opaque.
What this does not claim. The pipeline checks that the code matches its types, effects, and the formula it was generated from. It does not check that the formula models the right thing. Whether Black-Scholes is the correct model for a given book is a question for your risk function, not the compiler. See the trust stack for where the guarantees stop.
Path 2: from a requirement
A requirement someone signed off on becomes a property the compiler proves.
Not every guarantee starts as a formula. Some start as a sentence in a specification: a constraint a regulator, a clinician, or a risk function decided the system must hold to. C Proof takes that sentence onto the same substrate, as a property bound to the function it constrains.
1. The requirement, written in structured English
Requirements are written in the EARS form (Easy Approach to Requirements Syntax): constrained English with a fixed shape, so a requirement reads the way a person wrote it but parses the way a machine needs. Take a dosing constraint:
The system shall ensure that the calculated dose is non-negative.2. The property, bound to a function
The requirement becomes a Chelis property attached to the function it governs. It is not a comment and not a separate test file: it travels with the function, and the compiler treats it as part of what the function must satisfy to build.
property dose_non_negative(p: DoseParams) -> bool = ge(calculated_dose(p), 0)3. Verification, by the strongest method the math admits
The compiler discharges the property the strongest way the math allows. Where the property is decidable, it carries a formal proof that the implementation satisfies it for every input. Where a closed-form proof is out of reach, it falls back to seeded randomized testing across the input space, recorded with the seed so the run reproduces exactly. The property is the same either way; only the tier of evidence behind it changes.
4. An audit-ready certificate
What comes out is a certificate, not a green checkmark. It records the requirement it came from, the function it is bound to, the proof tier that discharged it (formal proof or seeded testing), and the evidence behind that tier. An auditor can read the requirement, follow it to the function, and see how the claim was established, without rerunning the pipeline.
What this does not claim. Verification proves the implementation satisfies the requirement. It does not prove the requirement describes what your business actually needs. A correct implementation of a wrong specification is still wrong code. See the trust stack for where the guarantees stop.
Path 3: from the code you already run
An existing Python codebase becomes Chelis, function by function.
Most teams are not starting from a blank file. Calcify translates an existing typed Python codebase into Chelis function by function: a mechanical translation where the types carry over cleanly, a mixed Python-and-Chelis program through the bridge where they do not, and documented decisions where a judgment call was required. Once a function is Chelis, the compiler enforces the same structural guarantees as hand-written code, and the same audit chain from source to binary applies. It is the modernization path for teams who cannot rewrite from scratch.
A typed Python function, the kind a team already runs:
def annualized_vol(variance: float, periods: int) -> float:
return sqrt(variance * periods)The same function after Calcify translates it into Chelis:
def annualized_vol(variance: f32, periods: f32) -> f32 = sqrt(mul(variance, periods))The types carry over, so a precision or shape error is a build failure on the Chelis side the same way it would be in hand-written code. Where a construct does not translate cleanly, Calcify leaves the boundary explicit rather than guessing, and the decision is recorded for review.