Verification Evidence🔗

Over the reals, the shifted ReLU below is flat at 1 for inputs at most 1 and grows with slope 2 above that point. It lets us compare a universal theorem, an evaluation, a membership check, and the theorem that relates acceptance to membership on the same function.

The definition is generic in the scalar type, as in the two-stage chapter. At \mathbb R it denotes a mathematical function; at Float it can execute on the host; at FloatLib binary32 it executes within a binary32 model. Context supplies the operations in each case. Sharing the definition keeps the expression aligned, while the scalar instance determines the meaning of its arithmetic.

6.000000

1.000000

true

false

@Box.containsDecBool_sound : ∀ {α : Type} [inst : Storage α] [inst_1 : Context α]
  [inst_2 : DecidableRel fun x1 x2 => x1 ≤ x2] {s : Shape} (b : Box α s) (x : Tensor α s),
  b.containsDecBool x = true → b.contains x

Example Commands🔗

These commands exercise the tensor, differentiation, graph, arithmetic, and certificate interfaces used in that chain:

# Compare tensor shapes and scalar representations.
lake exe torchlean quickstart_tensors
# Differentiate a tensor function and a model loss.
lake exe torchlean quickstart_autograd
# Train the small model from a stated seed and update
# budget.
lake exe torchlean quickstart_mlp \
  --device cpu --steps 200 --seed 2026
# Exercise eager execution of a graph-based model on CPU.
lake exe torchlean graphspec --device cpu --execution eager
# Compare evaluation and bounds attached to one operation
# graph.
lake exe torchlean one_semantic_universe
# Compare native Float32 values and derivatives with the
# executable reference.
lake exe torchlean float32_semantics
# Replay numerical evidence, including cases the checker
# must reject.
lake exe torchlean numerical_certificate

The first two stay close to concrete tensors. quickstart_tensors prints the same small array under four element types, which is the Context genericity from the previous section made visible at the command line:

== Quickstart: tensor basics ==
Rank-zero tensor: 0.500000
Float tensor:    [0.100000, 0.200000, 0.300000, 0.400000]
Rational tensor: [(1 : Rat)/10, (1 : Rat)/5, (3 : Rat)/10,
                  (2 : Rat)/5]
Integer tensor:  [1, 2, 3, 4]
Float32 cast:    [0.100000, 0.200000, 0.300000, 0.400000]
[two longer rank-3 lines elided]

The rational entry (1 : Rat)/10 is exactly one tenth. The Float entry is the nearest binary64 value to one tenth, and the Float32 cast entry is the nearest binary32 value. The two floating entries both print 0.100000, although they represent different numbers; the rational row displays its exact fraction.

quickstart_autograd then differentiates, first a tensor function and then a model loss:

== Differentiate a tensor function ==
mean(x^2) = 4.666667
d/dx       = [0.666667, 1.333333, 2.000000]

== Differentiate a model loss ==
loss     = 0.769887
gradient = [[1, 2]: [[-0.877432, 1.754865]],
            [1]: [-1.754865]]

The first gradient has one entry per input coordinate. The model-loss gradient has a weight row and a bias, matching the parameters with respect to which we differentiated. The two loss values belong to different objectives and cannot be compared as measures of model quality.

For x=(1,2,3) the mean of squares is \tfrac{14}{3}=4.\overline{6} and its gradient is \tfrac{2}{3}x, which is what the second line prints. The model gradient is tagged by parameter shape, [1, 2] for the weight and [1] for the bias, because a gradient in this repository is a shaped object rather than a flat vector; the autograd walkthrough takes that structure apart.

graphspec and one_semantic_universe then show why lowering matters: the same operation graph can be evaluated for values or interpreted for bounds.

The following transcript predates the FloatLib migration and retains its recorded scalar labels and numerical results. Current .ieee execution uses FloatLib binary32.

== One semantic universe tutorial ==
graph nodes = 6
[eval IEEE32Exec] y(x0) = 0.027713
[IBP IEEE endpoints] lo = -1.000000
[IBP IEEE endpoints] hi = 1.000000
consistency: 50/50 samples satisfied evalIEEE(x) ∈ IBP(B)
checker theorem:
  `NN.MLTheory.CROWN.Box.containsDecBool_sound`

The transcript reports one value, an interval, and 50 sampled membership checks, then names the checker soundness theorem. The interval [-1,1] is already a general range bound for the final \tanh activation; it gives no tighter information about this input box. The sampled checks do not establish that every input in the box is enclosed, and printing the theorem's name does not supply an acceptance proof.

In the same pre-migration record, float32_semantics compares host arithmetic with executable binary32 semantics. The two agree exactly on its example:

== Float32 (native runtime) ==
y   = [2.080000]
...
inputGrad  = [0.760000, 1.000000]
== IEEE32Exec ==
y   = [2.080000]
...
inputGrad  = [0.760000, 1.000000]
max_abs_diff(Float32 vs IEEE32Exec) = 0

Here y is the forward value, while inputGrad describes sensitivity to the two input coordinates. Checking both exercises the forward and backward calculations. The complete executable also compares the parameter gradients elided here. Its zero difference concerns this graph, these inputs, and this host; the FP32 soundness chapter develops the additional argument needed to relate native operations to the reference.

numerical_certificate exercises a graph-level checker and negative cases containing malformed evidence. Its output records which cases accepted or rejected; the associated soundness statement identifies the proposition obtainable from a formal acceptance witness.

Validation Commands🔗

The small demonstrations above explain individual ideas. Before relying on a larger change, use the validation command that reaches the relevant boundary:

# Compile and run the curated suite against the CPU CUDA stub.
lake build nn_tests_suite
lake exe nn_tests_suite

# Compile the native CUDA implementation, then execute it on a device.
lake -R -K cuda=true -K cuda_home=/usr/local/cuda build nn_tests_suite
CUDA_VISIBLE_DEVICES=0 lake env ./.lake/build/bin/nn_tests_suite

# Check native kernels for memory, race, and synchronization defects.
scripts/checks/cuda_sanitize_tests.sh \
  --all-tools --cuda-home /usr/local/cuda --skip-build

# Replay the default checked-artifact suite.
lake exe verify -- all

# Check conventions and rebuild the documentation site.
lake lint
scripts/docs/build_site.sh

A successful CUDA-enabled build establishes that the selected native sources compile and link. The runtime test also needs a visible CUDA device to exercise GPU execution. A theorem build checks Lean declarations, while certificate replay exercises parsers, policy gates, and stored artifacts. The documentation build checks that its elaborated examples and imports remain valid. Compute Sanitizer checks the tested binaries with memcheck, racecheck, initcheck, and synccheck; its results are specific to the executions it observes.

Read the coverage of these commands as carefully as their results. verify -- all runs ten sections, while verify -- list registers twenty-three tools, so a green all leaves thirteen registered tools untouched, including every torchlean-* workflow and the two-stage Lyapunov pipelines. That is a deliberate choice about runtime, not a claim that the rest passed. The same applies inside a section: margin-report finishes with

[margin report] examples=360
[margin report] nominal_ok=349 (requires 'pred' in examples)
[margin report] positive_margin=318

and exits zero. The report contains 318 positive margins among 360 entries. That count is distinct from the tool's internal consistency checks, and a successful exit does not establish that all 360 entries have a positive verified margin.

The three counts have different predicates. examples counts the entries inspected; nominal_ok depends on the available prediction field; positive_margin counts entries meeting the reported margin condition. A reader cannot infer from these totals alone which individual entries satisfy both conditions, or why an entry lacks one of them. In particular, exit status zero means the reporting workflow completed its own checks. It does not replace the application criterion that every required example, or every point in a specified region, must have a positive margin.

Verification Claims🔗

Suppose a colleague sends you a result that says:

The trained model is robust on a box of inputs.

To assess the claim, the artifact needs to identify:

1. Which model? Identify architecture, parameter artifact, and graph payload.

2. Which input box? Give lower and upper tensors with checked shapes.

3. Which robustness property? State the output inequality or class-margin condition.

4. Which scalar semantics? Exact real, finite FP32, executable IEEE32, or a native runtime.

5. Which method? IBP, CROWN, α,β-CROWN artifact replay, branch-and-bound, or another checker.

6. Which theorem? Name the proposition obtained when the checker accepts.

7. Which boundary remains trusted? Identify unproved assumptions about artifact identity, parsing, the backend, compiler, or hardware. A soundly checked certificate need not trust the search that proposed it.

For example, a certificate could establish that graph G, with parameter artifact P, has positive class margin Q throughout [\mathrm{lo},\mathrm{hi}] under exact real semantics. The evidence would include the checker's acceptance proof and the theorem deriving that margin from acceptance. Deploying a float implementation adds a separate obligation to preserve the margin after numerical error. Changing P, the input box, or the implementation changes which parts of this argument must be repeated.

For the shifted ReLU, the observed computation is (ccScalar : Float → Float) at input 3.5. The returned value 6 passes Box.containsDecBool for ccBox, whose bounds are 5.5\le y\le 6.5. Box.containsDecBool_sound would derive membership from a proof of that acceptance equality in the logical scalar model. This page records the host evaluation but does not supply that proof for ccBox. Connecting native evaluation to the logical model, and checking that both refer to the same value and box, are additional obligations. The check is point membership, not a bound over an input region.

0.300000

false

5.551115

Proof Modules🔗

Much of the argument can live entirely in Lean. Shapes and layer composition, mathematical operator specifications, graph well-formedness, autograd rules, generic rounding, finite FP32 mathematics, executable IEEE32 reference algorithms, optimizer laws, and checker soundness are all stated as named definitions or theorems with explicit hypotheses.

To find the statement behind a particular operation, use the corresponding source directory:

Start with the declaration supporting your claim and follow its imports and hypotheses. The existence of many nearby theorems does not prove a runtime implementation, and a thin API module can still expose a well-supported operation by delegating to a proved specification.

relu_deriv_correct : ∀ (x : ℝ), x ≠ 0 → HasDerivAt Activation.Math.reluSpec (Activation.Math.reluDerivSpec x) x

@round_abs_error_le_ulp : ∀ {β : Radix} {fexp : ℤ → ℤ} [inst : ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] (x : ℝ),
  |FloatLib.Floats.Formats.Flocq.round rnd x - x| ≤ ulp β fexp x

Numerical Guarantees🔗

For a numerical claim, choose the representation that retains the information the claim needs:

FloatLib.Floats.Formats.Flocq
  generic radix, format, and rounding mathematics; FloatRep and NF

FP32
  binary32-precision, gradual-underflow rounded-real semantics with no upper exponent cutoff

FloatLib.Floats.ExecFloat.Binary e f
  configured executable binary representation and operations
  8 23 gives binary32; 15 112 gives binary128; valid custom widths use the same API

The generic theory supports reasoning about spacing and rounding across formats (Boldo and Melquiond, 2011). Configured values also retain encodings and exceptional values. To connect either account to a CPU or CUDA run, we need the selected provider's contract.

Our closing function makes the distinction concrete. Evaluate it at binary64 and at the executable binary32 semantics, and report the difference in units of 10^{-9}:

(1.200000, 1.200000, 47.683716)

The tuple records the binary64 answer, the binary32 answer converted back for display, and the signed difference multiplied by a billion. The binary32 path first converts the input x, then evaluates the function in its chosen arithmetic. Its discrepancy therefore includes input representation as well as subsequent rounding. It cannot be assigned entirely to the final addition. Converting the binary32 result to binary64 exposes its value without restoring digits that the narrower path discarded. The positive last component says this path's answer is slightly larger for the particular input 1.1.

Both displayed values are 1.200000, but their difference is about 4.768\times 10^{-8}, roughly four tenths of a binary32 ULP near 1.2. The six-decimal display has rounded away the difference (Goldberg, 1991); comparing these strings would miss it.

The PyTorch computations captured before the FloatLib migration give the corresponding binary32 and binary64 values:

python3 - <<'PY'
import torch
for dtype in (torch.float32, torch.float64):
    x = torch.tensor([1.1], dtype=dtype)
    y = (2 * torch.clamp(x - 1, min=0) + 1).item()
    print(dtype, y.hex(), y)
PY
torch.float32 0x1.3333340000000p+0 1.2000000476837158
torch.float64 0x1.3333333333334p+0 1.2000000000000002

The binary32 result, converted exactly to binary64 for display, is 0x1.3333340000000p+0; the binary64 computation gives 0x1.3333333333334p+0. These match the two TorchLean evaluations on this input in that recorded comparison. This transcript is not a validation run of the migrated runtime. FloatLib binary32 makes the representation and operations explicit (Boldo et al., 2015); the comparison remains evidence for the tested expression and input.

Let f be the target function, F_{\mathbb R} the ideal real-valued network, and F_{\mathrm{runtime}} its runtime implementation. Interpreting both outputs in a common real space lets us split the total error:

|F_{\mathrm{runtime}}(x)-f(x)| \leq |F_{\mathrm{runtime}}(x)-F_{\mathbb R}(x)| + |F_{\mathbb R}(x)-f(x)|.

The first term is numerical implementation error. Rounding theorems at the FP32 or FloatLib binary32 level can contribute to its bound once the runtime is connected to that formal semantics. The second is model approximation error, addressed by the real-valued theory in Approximation Theory. Bounds on both terms must use compatible input domains and the same parameters to produce an end-to-end bound against f.

Configuration Validation🔗

Shape and configuration checks act at different stages. A typed expression can fail during elaboration, an external tensor can fail during parsing, and a command can reject an unsupported flag before starting its computation.

The first is elaboration. A shape error in a matrix product is not a runtime failure; the file does not compile. Here is a two by three tensor multiplied by itself:

Application type mismatch: The last
  ccA
argument has type
  Tensor Float [2, 3]
but is expected to have type
  Tensor Float [3, 2]
in the application
  ccA.matmul ccA

The inner matrix dimensions are 3 and 2, so multiplication is ill-typed. The elaborator reports the incompatible shapes before evaluation.

The second is parsing at a boundary. Shapes crossing from outside cannot be checked by the elaborator, because the payload is a string when the program is already running. The PyTorch state_dict importer therefore returns an option and we turn it into a message:

"[[1.000000, 2.000000], [3.000000, 4.000000]]"

The wrapper first asks whether the string is valid JSON, then asks whether that JSON has the nested numeric-array structure required by shape [2, 2]. A successful parse produces an actual tensor whose shape is known to Lean. The wrapper returns its formatted contents only to make the example easy to inspect. Its failure branch combines malformed JSON and an incompatible tensor payload into one message, so that message should not be treated as a precise diagnosis of every possible input error. A production loader can retain more detail from each stage.

A row of the wrong width is refused rather than truncated or zero-padded:

"refused: shape does not match [2, 2]"

So is a JSON object where an array was expected:

"refused: shape does not match [2, 2]"

The rejected matrix has two rows but three entries per row, so it fails the inner extent check. The object containing a weight key is syntactically valid JSON but fails a different requirement: this parser expects the tensor itself, not a state-dictionary wrapper. A caller handling such a wrapper must select the intended field before asking for a tensor. These checks establish the shape and encoding of the imported value. They do not establish that its numbers are the intended checkpoint or that the external model uses the same weight convention.

This wrapper gives the same message for a wrong row width and a wrong JSON kind because both become none. The importer's Except String variants retain more detail, allowing callers to distinguish missing keys, invalid JSON kinds, and incompatible shapes.

The third is the command line. Flags are parsed strictly, so an unknown flag stops the example rather than being ignored:

$ lake exe torchlean quickstart_tensors --show-backend
error: quickstart_tensors: unexpected arguments: [--show-backend]

Rejecting unknown flags prevents a requested device or arithmetic mode from being silently ignored. This message identifies the unexpected arguments; the command's help lists supported options.

Backend Contracts🔗

Large models rely on specialized matrix multiplication, convolution, attention, FFT, and communication libraries. TorchLean can specify those operations and dispatch to a provider, with an explicit contract for the values and derivatives that provider returns.

The graph fixes the computation, while the provider implements its numerical operations:

one semantic operation graph
  -> several admissible kernel providers
  -> explicit contract and evidence per boundary

TorchLean records graph structure, shapes, loss, optimizer meaning, and proof statements while a provider supplies a fast value or a local VJP. The assurance level ranges from a proved internal implementation to a checked or explicitly trusted external kernel, and the capsule says which.

Examples that dispatch backend operations can report their contracts with --show-backend:

$ lake exe torchlean quickstart_mlp --steps 3 --show-backend
== Quickstart: simple MLP training (seed=0, steps=3) ==
...
  matmul: reference.matmul provider=reference trust=checked
      vjp=torchlean-tape reduction=fixed-left
    shape: shape safety for matmul; guarded at runtime by portable
      runtime shape checks
    layout: canonical-tensor layout compatibility for matmul;
      guarded at runtime by typed tensor layout
    value: matmul forward refines its TorchLean semantics; covered
      by test suite NN.Tests.Runtime.Floats.Suite
    vjp: matmul torchlean-tape VJP refines its TorchLean semantics;
      covered by test suite NN.Tests.Runtime.Floats.Suite

Long lines are wrapped here; the tool prints one line per claim. provider=reference identifies the selected implementation, and trust=checked records test evidence. reduction=fixed-left specifies the summation order, which can affect floating-point results. The shape claim cites runtime checks, while the layout claim cites the typed tensor layout. The value and VJP claims name NN.Tests.Runtime.Floats.Suite as their evidence; these entries do not name refinement theorems.

The capsule makes it possible to inspect evidence per operation. Strengthening one entry from test coverage to a proof requires a theorem for the stated provider, semantics, and numerical policy.

The flag belongs to examples that perform backend dispatch. For example, quickstart_tensors --show-backend rejects it because that example does no dispatch. An unsupported flag is a usage error, not evidence that a different backend ran.

Scientific ML🔗

A PINN or neural operator usually participates in a larger chain:

equation and domain
  -> discretization or simulator
  -> dataset
  -> model and training
  -> prediction artifact
  -> residual, invariant, or error certificate
  -> Lean checker and theorem

The neural network is only one part. Boundary conditions, quadrature, sampling coverage, simulator accuracy, and interpolation between grid points can dominate the final claim. A residual that is small at the collocation points says nothing about the points in between unless something else supplies that step, and in the Fourier neural operator case the discretization is part of the operator rather than an implementation detail (Li et al., 2021).

A checker soundness theorem can connect an accepted artifact to a precise scientific claim. The external search or training process need not be repeated to validate a sufficient certificate (Necula, 1997). The resulting guarantee still depends on the encoded equation, domain, and assumptions matching the scientific problem.

Operation Development🔗

When adding an operation, define its tensor shapes and scalar semantics, then implement the runtime forward computation and derivative rule. Add an IR representation if the operation must participate in export, lowering, or graph verification.

Each provider needs a declared layout, numerical policy, and evidence level. Reusable semantic facts belong in theorems; rejection behavior also needs executable checks. A bad shape, nonfinite parameter, unsupported policy, or malformed artifact should fail for the documented reason. Recorded negative cases make that behavior reviewable.

Running a shared model through each claimed path checks whether its definition, derivative rule, lowering case, and dispatch agree on concrete inputs. Property-based and structure-aware fuzzing explore a wider range of such interactions (Odena et al., 2019) (Liu et al., 2023). These executions complement the declarations checked by Lean; a small example suite does not establish the same coverage as a fuzzing campaign.

Proofs establish propositions about formal objects under their stated hypotheses. Tests exercise wiring, FFI, builds, command lines, documentation, and platform behavior that those propositions may not cover. Validation should include the paths an application actually uses.

Application Requirements🔗

Start from the property your application needs, then follow its hypotheses through the model, arithmetic, and selected runtime. The earlier chapters give the relevant contracts beside the operations and checkers that use them. For example, a classifier needs a positive verified margin; an ODE candidate needs successful certificate replay over its stated domain. A training loss alone does not establish either property.

Use the public tensor API for numerical values and select a runtime with an implemented provider. Run the corresponding verification workflow and backend checks for your deployment. The command registry identifies which workflows verify -- all includes; additional workflows can be invoked individually.

Model Review Exercise🔗

Choose one example from the model collection and write down:

input and output shapes
parameter shapes
loss
data source and preprocessing
arithmetic
execution mode
device and selected providers
forward and backward implementation responsibility
available theorem or checker
remaining trusted assumptions

For an example that supports backend reporting, compare this record with --show-backend. The report identifies provider, trust level, reduction order, and evidence for dispatched operations. Loss definition, data provenance, and application assumptions must come from the model and workflow artifacts.

Compare the shifted ReLU in this chapter with a training workflow such as chargpt or fno1d_burgers. The former has a theorem over every real input but no training artifact; the latter adds parameter state, data, optimization, and backend choices. Identify which component theorems apply and which claimed connections still rely on tests or assumptions.

For a result built with TorchLean (George et al., 2026), record the exact model and artifact, the proposition established, and the evidence connecting that proposition to the selected runtime. Those identifiers let a later change to parameters, preprocessing, or backend be traced to the guarantees that need to be checked again.