An automated software factory.
We produce formally-verified SPARK-Ada code from prose specifications and legacy Fortran sources — the same verification regime used to certify aircraft flight-control software. Currently the only language our factory produces; we're finding out how large we can go.
69,775 lines of legacy scientific Fortran — seismic hazard, molecular dynamics, numerical linear algebra, wind-turbine control, ESA mission software — modernised into 23,236 lines of SPARK-Ada (spec + body), of which 95.7% of 19,960 proof obligations have been mechanically discharged by gnatprove + CVC5/Alt-Ergo — the same SPARK toolchain used to certify aircraft flight-control and rail-signalling software. Since 12 May 2026 — equivalent to roughly 76 person-years of conventional Ada/SPARK commissioning. US Federal seismic-hazard infrastructure, US academic numerical linear algebra, UK national-lab molecular dynamics, Danish wind-turbine control, European Space Agency mission software. See the portfolio →
Available as a drop-in capability for organisations needing formally-verified SPARK-Ada output — autonomous-vehicle stacks (ASIL-D), avionics (DO-178C), defence (Def Stan 00-055), industrial automation (IEC 61508), regulated public-sector. Deployable inside customer secure perimeters; per-chapter engagement, no per-user or per-subscription fees.
Liberty decisions, calculation engines, eligibility rules — provably correct
Software running in regulated and high-stakes government contexts should be provably correct. The factory produces it that way — to the same formal-verification regime used to certify aircraft flight-control and rail-signalling software.
SPARK-Ada eliminates whole classes of vulnerability at compile time — buffer overflows, integer overflows, use-after-free, race conditions. Aligns with NCSC's memory-safe-language guidance and offers a sovereign rapid-replacement path when legacy software is compromised.
Runs on UK infrastructure. Sensitive data stays inside your network. No US-cloud dependency. The verification and admission-gate layer is open source by design, so no single supplier — including us — can lock you in.
Factory engagements are priced per package or per project, not per user or per subscription. Outputs are released to the engaging party under a permissive licence appropriate to the source — Apache 2.0 for clean-room work, or the upstream licence for modernisations. No vendor fees on delivered code.
Boundary: What we deliver is the formally-verified substrate. Certification to DO-178C, Def Stan 00-055, IEC 61508, or equivalent regimes remains a customer-side procurement step. We provide a head-start on the substrate at a fraction of conventional cost.
Every item the factory has shipped, one square at a time
Each square below is an independent factory output. Four open into live worked-example calculators you can click through (marked live demo). The rest are Fortran modernisations and prose-spec builds — click any one to find its row in the portfolio production ledger with line counts, package counts, and verdicts.
Tell us what you want built.
The factory produces formally-verified SPARK-Ada from prose specifications and legacy Fortran. If you have software that needs modernising, or a regulated-sector deployment that needs SPARK-Ada substrate, email us. Every enquiry is read and answered by a human.
What to include in your email → tony.gair@thedarkfactory.co.uk