What the factory produces.

Thirteen SPARK-Ada packages implementing UK income tax for a calibration tier: Personal Allowance taper, Basic / Higher / Additional rate bands, dividend calculation, Gift Aid relief, High-Income Child Benefit Charge (HICBC), Marriage Allowance, National Insurance Class 1 / 2 / 4, pension relief, student loans (Plans 1 / 2 / 4 / 5 / Postgraduate), tax-year discrimination, and a CLI entry point. Every operation carries Pre/Post contracts; every band crossover and taper threshold is encoded as a verifiable invariant.

Why it matters: Tax law changes annually; HMRC publishes thousands of pages of guidance every Finance Act. Most tax-calculation software is hand-written in spreadsheet formulae or imperative code, where a band-edge bug can silently understate or overstate every taxpayer's bill for a year. A SPARK-Ada implementation lifts the verification regime from "we wrote tests" to "every band threshold and every taper rate is mathematically asserted at the type system level".

SPARK-Ada port of twelve core modules from DL_POLY Classic, the open-source molecular-dynamics package developed at STFC Daresbury Laboratory since 1992. Covers the heart of MD: velocity-Verlet and leapfrog rotation integrators (20,947 LoC, four modules), motion integrators (6,024 LoC, two modules), bonded and non-bonded force evaluation (3,309 LoC), hyper-dynamics for rare-event sampling (2,821 LoC), potential-of-mean-force (1,924 LoC), metal force fields (1,672 LoC), dihedral torsions (1,134 LoC), and the SHAKE constraint solver (157 LoC). Total: 37,988 LoC of UK national-lab Fortran 90 → 53 SPARK-Ada packages, all gnatmake -c clean. Several adjacent modules produced partial output (Coulombic forces, Ewald, neighbour-list construction, thermodynamic ensembles, path-integral MD, properties) and are queued for rework against the next factory-pipeline iteration.

Why it matters: DL_POLY is the UK's flagship open-source molecular-dynamics codebase — materials science, drug discovery, battery research, vaccine and veterinary pharmaceutical work, and protein dynamics all run on this tool or its derivatives. The factory demonstrates that a UK national-laboratory codebase three decades old can be modernised to memory-safe SPARK-Ada inside a single working session — UK-born software, modernised in the UK, running on UK hardware, ready for the next thirty years.

SPARK-Ada port of LAPACK 3.12.1's dgesvd.f — the singular-value decomposition driver for double-precision general matrices, written by the University of Tennessee and UC Berkeley LAPACK team. 3,552 LoC of dense numerical Fortran decomposed into four cohesive SPARK packages: argument validation, common types, magnitude scaling, and SVD orchestration. Every operation carries Pre/Post contracts over matrix shapes, leading dimensions, job-selector enumerations, and singular-value ordering invariants.

Why it matters: LAPACK is the substrate beneath MATLAB, NumPy, R, Julia, Mathematica, every quantitative-finance system, and every scientific HPC code on Earth. Memory-safety failures in LAPACK propagate everywhere downstream. A SPARK-Ada port of even a single major routine establishes the methodology: the foundation itself can be modernised, and the same arc applies to the rest of the library.

SPARK-Ada port of the Fortran codes that generated the published 2008 and 2014 USGS national seismic hazard maps for the conterminous United States. The upstream is a single 3,700-line monolithic Fortran program covering subduction-zone hazard computation — slab geometry, rupture-patch tiling, ground-motion prediction equations (Geomatrix 1995, Papazachos 2004, Strasser 2010, Atkinson-Macias 2009, Zhao et al., BC-Hydro), truncated-normal probability tables, deaggregation, and deterministic modes. Decomposed into eleven cohesive SPARK packages.

Why it matters: USGS itself has retired this codebase in favour of a modern Java rewrite. The factory demonstrates that a legacy science Fortran codebase of this scale — single-file monolithic, no separation of concerns, no formal interface — can be re-expressed as a clean, contract-bearing SPARK-Ada subsystem decomposition without hand correction. The same modernisation arc applies to every legacy scientific or industrial Fortran codebase a customer is sitting on.

SPARK-Ada port of DTU Wind Energy's open-source reference controller (DTUWEC) for pitch-regulated variable-speed wind turbines. Partial-load and full-load control loops, switching, drivetrain and tower dampers, rotor speed exclusion zones, de-rating, wind-speed estimation, individual pitch control, individual and cyclic flap control. Decomposed into a five-package SPARK structure.

Why it matters: Wind turbine controllers run on operational fleets for twenty years; the controllers are safety-rated and certified, the failure modes include blade-loss and tower collapse, and the original Fortran is still being maintained because rewriting it is expensive and risky. A SPARK-Ada port retains the original control law line-for-line while gaining contract verification, memory-safety by construction, and a substrate amenable to formal proof of stability properties. The same arc applies to every aerospace, automotive, or industrial controller sitting in legacy Fortran today.