The language semantics are mechanized in a proof assistant.

The five theorems

Four of these are stated and proved against the formal semantics with no remaining assumptions: type soundness, dimension safety, effect correctness, and linearity soundness. The fifth, automatic differentiation, is proved against an abstract model of the primitive derivatives rather than against concrete tensors. The statements below describe what each one rules out, and the AD section is explicit about where its proof stops.

Type soundness: progress and preservation

Stated as two theorems. Progress: a well-typed program is either a value or can take a step. It does not get stuck. Preservation: when a well-typed program takes a step, the result still has the same type. Together they rule out the class of error where a program in a valid state reaches an operation it cannot perform.

Dimension safety: dimension_safety

A well-typed program has no primitive shape mismatch. The named tensor dimensions the type system tracks are sound: a dimension error is not a run-time exception that survived testing, it is a state the type system proves cannot arise.

Effect correctness: effect_correctness

A well-typed program never gets stuck on an effect it tried to perform without the capability to perform it. The effect annotations are not documentation. They are a checked contract the proof backs.

Linearity soundness: linearity_soundness

Stepping a well-typed program preserves a well-formed store. The ownership and resource discipline the type system enforces holds as the program runs, so the memory and device resources a program tracks stay consistent across every step.

Automatic differentiation: ad_correctness

For pricing and risk, where the Greeks are derivatives of a price, a wrong gradient is a wrong hedge. This theorem addresses that case, and it is the one place on this list where the proof is conditional. It is stated against an abstract model of the primitive derivatives: a package of per-primitive derivative laws the proof assumes hold. Given those laws, it establishes that the adjoint the compiler generates satisfies the model's gradient-correctness relation for the typed first-order grad fragment.

What is not yet closed is the link from that abstract model to concrete tensors. The mechanization states this directly: the abstract package is not instantiated, and a concrete tensor model still has to supply the denotational ingredients, without further assumptions, before the gradient-correctness statement becomes a closed theorem about real tensors. So the AD result is a proof that the generated adjoint is correct relative to assumed primitive laws, not yet a closed proof that the gradient the machine returns equals the gradient the mathematics defines. Closing that gap is open work.

Why a mechanized proof matters to a buyer

A test suite shows that the cases someone thought to write pass. A mechanized proof shows that no case fails, because the proof assistant will not accept the theorem otherwise. The difference is the gap between "we did not find a counterexample" and "a counterexample cannot exist."

When the binary prices a book, that gap is the risk. Your engineers can read the compiler. Reading it line by line does not establish that the type system it implements is sound. The proof does, and a person who does not read the proof assistant can still know that the soundness claim was checked by a machine that does not get tired, does not assume, and does not wave through the case nobody tested.

What the proof does not cover. It is a proof about the language. It bounds what the runtime can do to a program. It does not judge whether the program prices the right model under the right assumptions. That question stays with your risk function. See the trust stack for where each guarantee stops.