For UK Government
The Dark Factory automates the production of memory-safe SPARK-Ada code. Every output unit declares SPARK_Mode => On and is processed by the same toolchain (gnatmake, gnatprove with CVC5 and Alt-Ergo) — established tools that are openly available, so the evidence travels with the code and can be re-checked by anyone holding the same toolchain. Across the current 29-source corpus, the proportion of proof obligations mechanically discharged varies by source and is published per source on the results pages — it is not 100%, and we do not quote a single aggregate figure for it. The residuals are obligations gnatprove flags for human review, typically loop invariants and overflow bounds. A dedicated per-engagement proof pass is how those get closed; until one has been run for a given source, they are open.
The Dark Factory produces software whose behaviour is written down as machine-checkable contracts and then checked by a prover, using openly available proof tools rather than tooling only we can run — so the evidence is something you can re-check rather than take on trust. That is not the same as a guarantee of correctness, and we do not claim one. What we publish, per source, is how many proof obligations were discharged and how many were not. Where something is not proved, it is labelled not proved.
The factory's initial output is a safety-infrastructure stack for UK public-sector deployment. Runs on UK on-premise infrastructure with no SaaS dependency. The same pattern generalises: the factory can be commissioned to produce SPARK-Ada replacements for decision-logic or calculation-engine layers in any department or regulated sector requiring formal verification of correctness under SPARK 2014.
The factory's first published outputs are safety calculators for UK public-sector use. They run on UK hardware and your data never leaves your own network. The same approach generalises: the factory can be commissioned to rebuild any department's decision-logic or calculation software with mathematical guarantees of correctness.
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 — prompt injection emitting hidden malicious code that passes ordinary review and reaches production. The factory's safety layer is built in SPARK-Ada under SPARK_Mode => On; proof obligations and contract checks catch this class of attack at the type-and-compile level before any output reaches the admission gate.
AI coding tools have a known vulnerability: a malicious instruction can make the model emit hidden harmful code that slips past human reviewers. The factory's outputs go through a proof layer before they're accepted — a mathematical proof rather than a review or a test suite — which catches this class of problem before any code is released.
Beyond AI specifically: formally-verified SPARK-Ada eliminates whole classes of memory-safety obligation by construction — buffer overflows, integer overflows, use-after-free, data-race obligations, aliasing violations — the classes that account for roughly 70% of CVEs in mainstream software. When a Log4Shell-class vulnerability lands in a decision-logic system, the factory enables rapid rewrite of the affected component in chapter-time rather than weeks of vendor-patch wait. Aligns with NCSC's published memory-safe-language guidance.
Beyond AI specifically: SPARK-Ada removes whole categories of software defect by construction — the memory errors responsible for around 70% of publicly recorded security vulnerabilities in mainstream software cannot be written in it in the first place. That is a property of the language, not a claim about any particular delivery: where a specific output still carries undischarged runtime checks, we publish that count rather than round it away. When a widespread vulnerability is found in a piece of legacy software, the factory can produce a replacement quickly rather than waiting weeks for a vendor patch. This approach aligns directly with NCSC's published guidance.
Deployment
Runs on UK on-premise infrastructure with no cloud egress. The factory toolchain (Ada/SPARK compiler, gnatprove, admission gates) can be packaged for installation on your own infrastructure and operated by your own engineers, inside your own network boundary.
Runs on UK hardware. Sensitive data never leaves your own network. The whole factory can be installed on your own systems and run by your own engineers — no external service to depend on.
Factory output
Four worked-example chapters are publicly hosted at the URLs below. For each, the SPARK-Ada specification is authored by hand (the planner stage — an automatable extension point); the factory generates the implementation against it, and every gnatprove obligation is discharged (the release calculator: 31 of 31, zero unproved, zero assumptions). Anyone can clone the source and re-run the proof obligations against the published artefacts. Three are liberty-decision use cases modelled from published rules — the precise class of problem that has historically justified formal verification, because errors produce human-rights consequences. None are commissioned by, deployed in, or endorsed by any government department; they are independent demonstrations.
Four worked-example calculators are publicly hosted at the URLs below. For each, the specification is written by hand; the factory then produces the software that satisfies it and proves it correct, with every proof obligation discharged. Anyone can visit them and check the output is what the published rules say it should be. Three of the four are liberty decisions (prisoner release dates, Home Detention Curfew, parole) modelled from published rules — the kind of decision where errors have real human-rights consequences. None are commissioned by, deployed in, or endorsed by any government department; they are independent demonstrations.
- 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: hand-authored SPARK-Ada specification (the planner stage) under SPARK_Mode => On → gnatmake-clean factory-generated body → gnatprove-discharged (zero unproved, zero pragma Assume) → publicly hosted. The human writes the specification; the factory writes and proves the code beneath it. Body generation and proof: 30–45 minutes per chapter.
For each calculator, the specification is written by hand; the factory then produces the code that satisfies it and proves it correct, with every proof obligation discharged and none assumed. The machine writes and proves the implementation; the human writes the specification it must meet.
Important boundary
The factory delivers the memory-safe SPARK-Ada substrate of high-assurance software — output declares SPARK_Mode => On, compiles clean under gnatmake, and is processed by gnatprove with CVC5 and Alt-Ergo. Across the current 29-source corpus the factory ships output with proof obligations machine-discharged out of the box; the residuals (loop invariants, overflow bounds, complex quantified obligations) and final certification against whichever assurance regime applies to your sector, assessed independently, remain customer-side procurement steps. The factory offers a substantial head-start on the substrate — not a pre-certified deliverable.
The factory delivers the SPARK-Ada source and its proof evidence — code that compiles clean, together with the prover's report of which safety properties were discharged and which were not. Across the current portfolio that proportion varies by source and is published per source; it is not 100%. The residual ones are properties flagged for a human reviewer, and the full assurance process for your sector, against an independent assessor, remains a customer-side step. The factory gives you a substantial head-start on the foundation — not a pre-certified product.
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 source licence (BSD-3, MIT, OGL v3.0, etc.) honoured 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 artefact.
Factory outputs are released to the customer under an open licence — typically a permissive open-source licence that allows free use, modification and redistribution. Whoever commissions the work owns the right to deploy, modify and run it without ongoing fees or vendor lock-in.
The factory itself — the automated production pipeline that turns prose specs into formally-verified SPARK-Ada — is The Dark Factory Ltd's commercial capability.
Deployment model
The factory can be packaged for installation on your own hardware, inside your own network, and operated by your own engineers. Specifications, generated SPARK-Ada artefacts, and the gnatprove toolchain stay within your boundary — no cloud, no external dependency, and nothing of yours leaving the estate it started in.
The whole factory — toolchain, specifications, generated code — can be installed on your own systems and run by your own people. Nothing has to cross your network boundary; no cloud, no external service.
This addresses a deployment shape that is uncommon in formal-methods work: the production and the proving both happen where the data already is, rather than the data being sent to where the tooling lives. It fits departments holding records they cannot send anywhere — casework, benefits, tax, licensing, registers — and it removes the usual objection that modernising a system means first exporting it.
It fills a gap in how this kind of software gets made: the work and the checking both happen inside your own walls. That suits any department holding records it cannot send out, and it removes the usual blocker, which is that improving a system normally means letting it leave the building first.
Get in touch
For procurement enquiries, sector partnership discussions, or to commission a custom chapter against your department's requirements: