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) used to certify aircraft flight-control under DO-178C and rail signalling under EN 50128. Across the current 29-source corpus, 95.7% of 19,960 proof obligations have been mechanically discharged — the residual 4.3% are obligations gnatprove flags for human review (typically loop invariants and overflow bounds that a dedicated per-engagement proof pass would carry to 100%).
The Dark Factory automatically produces software that is mathematically proven to do what it says. Every piece of output is checked by the same proof tools used to certify aircraft flight-control software. Across 29 different code projects produced so far, 95.7% of nearly 20,000 individual safety properties have been verified automatically — the remaining 4% are properties the proof tool flags for a human to review.
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 mathematical proof layer before they're accepted — the same kind of proof used to certify aircraft software — 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: the factory's code is mathematically guaranteed to be free of the most common categories of software bug — those responsible for around 70% of publicly recorded security vulnerabilities in mainstream software. When a widespread vulnerability is discovered in a piece of legacy software, the factory can produce a verified replacement quickly rather than waiting weeks or months 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 inside government secure facilities and operated by departmental engineers cleared to the required standard.
Runs on UK hardware. Sensitive data never leaves your own network. The whole factory can be installed inside government secure facilities and operated by your own engineers — no external service to depend on.
Factory output
Four worked-example chapters are publicly hosted at the URLs below — each a complete factory run from prose specification through gnatprove-clean SPARK-Ada to live URL in 30–45 minutes wall-clock. 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 — each one a complete factory run from a written specification to a live web page in 30–45 minutes. 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 built end-to-end through the factory pipeline: prose spec → SPARK-Ada under SPARK_Mode => On → gnatmake-clean → gnatprove-discharged → publicly hosted. Wall-clock production: 30–45 minutes per chapter from spec to live URL.
Each calculator is built end-to-end through the factory's automated pipeline: written specification → mathematically-proven software → published live. Typical production time: 30–45 minutes from spec to live web page.
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 95.7% of proof obligations machine-discharged out of the box; the residual 4.3% (loop invariants, overflow bounds, complex quantified obligations) and final certification to DO-178C, Def Stan 00-055, IEC 61508, EN 50128, or equivalent regimes against an independent assessor remain customer-side procurement steps. The factory offers a substantial head-start on the substrate — not a pre-certified deliverable.
The factory delivers the mathematically-proven software itself — code that compiles clean and whose safety properties have been verified by automated proof. Across the current portfolio, 95.7% of safety properties are automatically proven out of the box. The remaining 4% are properties flagged for a human reviewer, and the full safety-certification process (DO-178C for aircraft, Def Stan 00-055 for UK defence, IEC 61508 for industrial) 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 inside UK government secure facilities, operated by departmental engineers cleared to DV, EDV, or STRAP standards. Specifications, generated SPARK-Ada artefacts, and the gnatprove toolchain stay inside the secure perimeter — no cloud, no external dependency at classified levels.
The whole factory — toolchain, specifications, generated code — can be installed inside UK government secure facilities and operated by government engineers with the appropriate security clearance. Nothing crosses the secure perimeter; no cloud, no external service.
This addresses a deployment shape that doesn't currently exist for most secure-environment formal-methods work: rapid, audited SPARK-Ada production by cleared personnel inside the perimeter 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.
This fills a gap in how secure-environment software gets made today: fast, mathematically-verified software production by cleared staff, inside the facilities where the work needs to happen. Particular fit for MOD / DSTL, NCSC, GCHQ, and MoJ secure environments — places where bringing in outside consultants is slow and expensive, and where sending code outside is not allowed.
Get in touch
For procurement enquiries, sector partnership discussions, or to commission a custom chapter against your department's requirements: