LAProof is a modular, portable proof layer between the verification of application software and the verification of programs implementing operations defined by the basic linear algebra subprograms (BLAS) specification.
See: the paper in 30th IEEE International Symposium on Computer Arithmetic (ARITH '23) or non-paywall version
LAProof provides formal machine-checked proofs of the accuracy of basic linear algebra operations:
inner product using conventional multiply and add, inner product
using fused multiply-add, scaled matrix-vector and matrix-matrix
multiplication, and scaled vector and matrix addition. LAProof error bounds are backward error
bounds and mixed backward-forward error bounds that account
for underflow, proved subject to no assumptions except a low-
level formal model of IEEE-754 arithmetic. We treat low-order
error terms concretely, not approximating as
The LAProof repository contains a machine-checked correctness proof of a C function implementing compressed sparse row matrix- vector multiplication as an example of connecting LAProof to concrete programs.
LAProof 2.0beta1 is based more directly on MathComp; that is, matrix and vector operations use definitions in mathcomp.algebra.matrix.