Results · Per routine

Eleven routines, exposed.

For every routine on the OWI ladder, this page gives the original Fortran (linked to its source), the Ada spec the factory emitted, the Ada body the factory emitted, and a short paragraph on what shape the result took. Nothing about how — that is on the methodology page. The page grows as new phases land.

Aggregate (Phase 1 + Phase 2 cfftf, strong postcondition): 4,424 obligations · 436 unproved · 90.1% discharged at gnatprove --level=1. Field-notes on the spread: Where the prover pushes back hardest. Methodology and what these numbers mean: /built-with-claude.html. Re-run the proofs yourself: verifier kit.

Phase 1

Foundational numeric ladder — BLAS L1/L2/L3 plus LAPACK LU, QR and Cholesky.

The ten kernels any safety-critical numerical stack ultimately sits on top of. Fortran sources are Netlib reference BLAS and LAPACK (Modified BSD).

ddot — double-precision dot product

349 obligations 22 unproved 93.7% discharged

Sum of pairwise products of two vectors with configurable strides. The strong test is harder than the April version; the score reflects that. Closure on the remaining 22 is bounded engineering.

daxpy — alpha · X + Y

294 obligations 15 unproved 94.9% discharged

Vector scalar-multiply-add: y[i] := alpha * x[i] + y[i] for every selected pair. 15 unproved obligations; bounded closure.

dscal — in-place scalar multiply

216 obligations 25 unproved 88.4% discharged

x[i] := alpha * x[i] for every selected element. 25 unproved obligations; bounded closure.

dnrm2 — Euclidean norm with overflow-safe scaling

292 obligations 23 unproved 92.1% discharged

L2 norm of a vector, with overflow-safe rescaling for very large and very small magnitudes. 23 unproved obligations; bounded closure.

dgemv — general matrix-vector product

399 obligations 46 unproved 88.5% discharged

y := alpha * op(A) * x + beta * y, with op selecting transpose-or-not. 46 unproved obligations; bounded closure.

dger — rank-1 update (outer product) manual patch

374 obligations 42 unproved 88.8% discharged

A := alpha * x * y^T + A. Adds an outer product to a matrix. This one needed a one-line manual patch on the emitted spec; the underlying gap in the pipeline is logged for a structural fix and a clean re-run.

dgemm — general matrix-matrix product

449 obligations 79 unproved 82.4% discharged

C := alpha * op(A) * op(B) + beta * C. The hardest test in the set; the score reflects that. Closure on the remaining 79 is bounded engineering work.

dpotrf — Cholesky factorisation

430 obligations 48 unproved 88.8% discharged

Factors a symmetric positive-definite matrix as A = L · L^T (lower-triangular). The body now serves the re-verified Cholesky factorisation against the same tightened audit dgeqrf received; the small dip from the earlier 90.2% figure reflects the harder test.

dgeqrf — QR factorisation

432 obligations 54 unproved 87.5% discharged

QR factorisation. The earlier 98.7% figure on this routine was withdrawn after an internal audit found the body satisfied its specification without doing the underlying Householder work. The body now serves a re-verified Householder factorisation against a tightened specification; 87.5% is the honest figure on the harder test.

dgetrf — LU factorisation with partial pivoting

528 obligations 34 unproved 93.6% discharged

P · A = L · U. LU factorisation with partial pivoting. Re-verified under the same audit treatment as dgeqrf and dpotrf; the body now serves a factorisation checked against a known-input reconstruction at runtime.

Phase 2

Signal and control kernels.

The signal-processing layer that surrounds the perception network in any autonomous-systems deployment. cfftf is rerun under strong postconditions; the three textbook control routines (Kalman, PID, quaternion) sit at the April baseline and are queued.

cfftf — forward complex FFT (full bundle)

661 obligations 48 unproved 92.7% discharged

Cooley-Tukey mixed-radix forward complex FFT (radix 2, 3, 4, 5). 48 unproved obligations; bounded closure. The Fortran is the original Netlib FFTPACK bundle (1985, public domain); the Ada is a single consolidated package covering cfftf, cffti, cfftf1, cffti1, and the passf* pass functions.

Phase 3

Inference kernels — int8 quantisation and FP-precision layers.

The cuDNN-shaped operations: int8 matmul and conv2d (quantised), plus FP64 conv2d, pooling, activation and normalisation. Unlike Phase 1 and Phase 2, where the Fortran is real published code (Netlib reference BLAS / LAPACK / FFTPACK), the Phase 3 reference Fortran was hand-written as a textbook implementation for the purpose — there is no public "reference int8 matmul in Fortran". The Fortran files are linked per row below; they are short (40–70 lines each), released into the public domain, and intended to be the verifiable mathematical baseline against which the emitted Ada is judged.

int8_matmul — symmetric per-tensor int8 × int8 → int32 matrix product

559 obligations 24 unproved 96.0% discharged

Reference: Jacob et al., Quantization and Training of Neural Networks for Efficient Integer-Arithmetic-Only Inference, arXiv:1712.05877 (2018). Symmetric per-tensor formulation, both input zero-points fixed at zero. 24 unproved obligations; bounded closure.

int8_conv2d — symmetric per-tensor int8 × int8 → int32 2D convolution

512 obligations 38 unproved 92.6% discharged

Reference: same Jacob et al. quantisation scheme applied to direct 2D convolution. Stride 1, no padding (valid). 38 unproved obligations; bounded closure.

conv2d_fp64 — FP64 2D convolution

453 obligations 49 unproved 89.2% discharged

Reference: standard FP64 direct convolution; see e.g. Goodfellow, Bengio, Courville, Deep Learning (2016), ch. 9. Lowest Phase 3 discharge; the score reflects the test being harder on the heavier shape. Closure on the remaining 49 is bounded engineering.

max_pool — 2D max pooling, configurable window and stride

384 obligations 36 unproved 90.6% discharged

Reference: standard CNN max-pooling layer; cuDNN's CUDNN_POOLING_MAX shape. Multi-channel input, configurable window and stride. 36 unproved; bounded closure.

relu — rectified linear unit activation

261 obligations 15 unproved 94.3% discharged

Reference: V. Nair and G. Hinton, Rectified Linear Units Improve Restricted Boltzmann Machines, ICML 2010. Element-wise y[i] := max(0, x[i]). 15 unproved; bounded closure.

layernorm — layer normalisation, single row

405 obligations 23 unproved 94.3% discharged

Reference: Ba, Kiros, Hinton, Layer Normalization, arXiv:1607.06450 (2016). Per-row mean / variance / affine transform via the learnable scale and shift. 23 unproved; bounded closure.

What lands here next.

Three control kernels (Kalman, PID, quaternion) are queued for rerun; they sit on the OWI page at the April baseline. Phase 4 (a wider set of FP inference layers and additional int8 quantised primitives) is queued. The page grows as the work does.