routine                obligations   unproved   discharge%
---                            ---        ---          ---
blas-ddot                      349         22         93.7%
blas-daxpy                     294         15         94.9%
blas-dscal                     216         25         88.4%
blas-dnrm2                     292         23         92.1%
blas-dgemv                     399         46         88.5%
blas-dgemm                     449         79         82.4%
fftpack-cfftf                  661         48         92.7%
lapack-dpotrf                  430         48         88.8%
lapack-dgeqrf                  432         54         87.5%
lapack-dgetrf                  528         34         93.6%
phase3-relu                    367         22         94.0%
phase3-max_pool                434         48         88.9%
phase3-layernorm               405         23         94.3%
phase3-conv2d_fp64             489         28         94.3%
phase3-int8-matmul             559         24         96.0%

Notes:
- Numbers are at gnatprove --level=1 against the .ads/.adb pairs
  in routines/<name>/.
- The "unproved" column is the count of proof obligations the
  prover could not discharge at this level. None are body-correctness
  failures on the routines in this kit; see README.md for the
  three classes of unproved residue.
- blas-dger and phase3-int8-conv2d are on the public /results/ page
  but are NOT in this kit — their gnatprove outputs were not saved
  during the last rerun and are queued for re-execution.
- Phase 4 (softmax, attention, transformer block) are on the public
  /results/ page but not yet in this kit — they are very new and
  their published artefacts will be added in a kit refresh shortly.