For UK Government
The Dark Factory automates the production of memory-safe SPARK-Ada code. Every output carries the SPARK_Mode aspect and is run through the same toolchain (gnatmake, gnatprove) used to certify aircraft flight controls and rail signalling. Across the current 29-source corpus, 95.7% of 19,960 proof obligations have been mechanically discharged by gnatprove with CVC5 and Alt-Ergo — the remaining 4.3% are obligations gnatprove flags for human review (typically loop invariants and overflow bounds that a per-engagement proof pass would take to 100%).
The factory's initial output is a sovereign AI safety infrastructure stack for UK public-sector deployment — for departments and regulated sectors that cannot safely use US commercial AI on sensitive data. It runs on UK hardware, keeps sensitive data inside the user's own network, and has no dependency on Microsoft Azure, Amazon Web Services, Google Cloud, or NVIDIA's commercial AI stack. The same pattern generalises: the factory can be commissioned to produce SPARK-Ada replacements for any US-vendor decision-logic or calculation-engine layer where UK sovereignty matters — making the Cabinet Office's sovereign-tech strategy economically and politically feasible.
Built by a founder with UK civil-service background. The initial demonstration chapters were chosen from inside knowledge of where safety-critical decisions actually sit in government — prison-service decisions on release dates, Home Detention Curfew, and parole, where errors have human-rights consequences. These are precisely the class of decisions Britain has always required formal procedure for; the factory brings the same proof-based rigour to the software that informs them.
What it addresses
Cybersecurity
Current AI coding tools have a category of vulnerability where prompts can be crafted to make models emit hidden malicious code that passes ordinary review and reaches production. The Dark Factory's safety layer is built in SPARK-Ada under SPARK_Mode — the same language and toolchain used to certify aircraft software — and catches this class of attack at the language-and-compile level.
Beyond AI specifically: formally-verified SPARK-Ada eliminates whole classes of memory-safety bug by construction — the classes that account for roughly 70% of CVEs in mainstream software. When a Log4Shell-class vulnerability lands in a US-vendor decision-logic system, the factory enables rapid sovereign rewrite of the affected component in chapter-time, rather than weeks-to-months of waiting for a vendor patch. Aligns directly with NCSC's published guidance recommending memory-safe languages.
Sovereignty
The system runs on UK hardware. Sensitive data stays inside the user's own network. No dependency on Azure, AWS, GCP, or NVIDIA's commercial AI stack. UK public-sector cloud and AI spend with US-owned providers currently runs to billions of pounds annually; this work removes that dependency for the most sensitive use cases.
Cost
Factory engagements are priced per chapter, 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 of existing open-source code. Whoever commissions a chapter can deploy and modify it without ongoing per-user fees, subscriptions, or vendor lock-in. Chapter-time engagement is materially cheaper than conventional safety-critical procurement.
Factory output
Four worked-example chapters are publicly hosted at the URLs below — each one a complete factory run from prose specification to live URL in 30–45 minutes wall-clock. Anyone can visit, inspect the output, and verify the SPARK-Ada is producing the claimed results. Three were deliberately chosen as liberty-decision use cases modelled from published rules: historically the precise class of problem that justifies formal verification, because errors produce human-rights consequences rather than just regulatory ones. None of these chapters are commissioned by, deployed in, or endorsed by any government department; they are independent demonstrations of what the factory can produce.
- hmpps-release-demo.thedarkfactory.dev — prisoner release date calculation [worked example · liberty]
- hdc-demo.thedarkfactory.dev — Home Detention Curfew eligibility [worked example · liberty]
- parole-demo.thedarkfactory.dev — parole eligibility [worked example · liberty]
- state-pension-demo.thedarkfactory.dev — State Pension eligibility [worked example · benefits]
Each chapter is built end-to-end through the Dark Factory's automated pipeline: prose specification → SPARK-Ada code under SPARK_Mode → compile-gated → publicly hosted. Typical wall-clock production time: about 30–45 minutes per chapter from spec to live URL.
Important boundary
The Dark Factory produces the memory-safe substrate of high-assurance software — SPARK-Ada code carrying the SPARK_Mode aspect, run through the same toolchain (gnatmake, gnatprove) the industry uses. Across our current portfolio, the factory ships output with 92.5% of proof obligations machine-discharged out of the box; the residual 7.5% (loop invariants, overflow bounds) and final certification to DO-178C, Def Stan 00-055, IEC 61508, or equivalent regimes are customer-side procurement steps conducted in the conventional way with an independent assessor. What we offer is a head-start on the substrate at a fraction of the conventional commercial commissioning cost — not a pre-certified deliverable.
Licence model
Factory outputs are released to the engaging party under a permissive licence appropriate to the source — typically Apache 2.0 for clean-room work, or the upstream licence (BSD-3, MIT, etc.) for modernisations of existing open-source code. Whoever commissions a chapter can deploy and modify it without ongoing fees or vendor lock-in on the delivered work.
The factory itself — the automated production pipeline that turns prose specs into formally-verified SPARK-Ada — is The Dark Factory Ltd's commercial capability. Engagement is per chapter, not per user or per subscription.
Deployment model
The factory can be packaged for installation inside UK government secure facilities, operated by government's own software engineers cleared to DV, EDV, or STRAP standards. Specs, generated code, and the toolchain itself stay inside the secure perimeter — no cloud, no external dependencies in classified mode.
This addresses a deployment shape that doesn't currently exist for most sovereign-tech work: rapid, formally-verified SPARK-Ada production by cleared personnel, in the environments where the work actually needs to happen. Particular fit for MOD / DSTL, NCSC rapid-response, GCHQ, and MoJ secure-environment work — domains where outsourcing to consultancies with cleared staff is slow and expensive, and where code crossing the perimeter is not an option.
Get in touch
For sovereign-AI procurement enquiries, sector partnership discussions, or to commission a custom chapter against your department's requirements: