Investor relations.

Where we are

In a paragraph

We build an automated software factory that turns prose specifications and legacy Fortran into formally-verified SPARK-Ada under SPARK_Mode => On. SPARK 2014 is the verification regime used to certify aircraft flight-control (DO-178C) and rail-signalling (EN 50128); the factory produces code in that regime, gnatprove-discharged with CVC5 and Alt-Ergo. The factory has been demonstrated in two output classes to date:

We build an automated software factory that turns plain-English specifications and old scientific code into modern software that is mathematically proven to do what it says. The same proof regime used to certify aircraft flight-control software. The factory has been demonstrated in two output classes to date:

• Government-shaped decision logic — four public worked examples (release-date / HDC / parole / state pension calculators); one of these accepted by HMG as a gift under the Open Government Licence v3.0. These model published rules; they are not commissioned deployments.
• Scientific numeric kernels — the foundational layer that safety-critical numerics sit on top of. Ten BLAS / LAPACK routines plus an FFT, spec + body, 90.1% aggregate gnatprove discharge at --level=1 under a stricter test than we asked in April; the body does the actual work. Three further textbook control routines (Kalman, PID, quaternion) sit on the page at the earlier baseline and are queued for rerun. Methodology and current numbers at /built-with-claude.html.
• Scientific numeric kernels — the low-level mathematical building blocks that safety-critical software sits on top of. Ten linear-algebra routines plus a Fourier transform, with 90.1% of their safety properties automatically proven correct. Three additional textbook control routines (Kalman, PID, quaternion) are also on the page at an earlier verification baseline and are queued for re-checking. Methodology and current numbers at /built-with-claude.html.

See the home page and the production ledger for full detail.

The honest negative side.

Investor pages typically lean into the positive. The straight version of where we are:

• No paying customers. Pre-revenue. The HMPPS sentence-release calculator was gifted, not contracted.
• No formal industrial partnerships. Our only formal relationship today is the downstream-customer one with Anthropic (we run their Claude models inside our pipeline). NVIDIA Inception is a pending application; AdaCore is not a partner; no defence prime is engaged commercially. Discussions are scoped under "obvious candidates we are seeking conversations with."
• No outside funding. Bootstrapped from founder time and UK hardware. Activate Founders application ready to fire, NVIDIA Inception decision pending.
• No deployed system at production scale. The factory works; the live demonstrators are worked examples modelling published rules, not running on departmental infrastructure.
• One person. The founder, plus the AI agents the founder built. No hiring planned ahead of customer revenue.

Each of those is a real gap and we will not pretend otherwise on this page. The technical capability is what is real today; the commercial and institutional surrounding is what we are working towards.

Public artefacts

We prefer evidence to claims. Things any prospective investor can inspect today:

• Release-date calculator — formally verified worked example, live demo
• HDC eligibility calculator — worked example, live demo
• Parole eligibility — worked example, live demo
• State Pension eligibility — worked example, live demo
• Public source: release-date calculator on GitHub — SPARK 10/10 obligations discharged
• Portfolio + production ledger — every Fortran source the factory has modernised, row by row, with verdicts

Note: the liberty-decision calculators are independent worked examples modelling published rules. They are not commissioned by, deployed in, or endorsed by any government department.

What we're doing about capital

Honest position: we are not currently running a structured raise. The next twelve months are about producing more verified artefacts and landing first customers — not about chasing capital ahead of those. Customer revenue and public-sector adoption will set our valuation and our terms more truthfully than a deck would.

That said, the door is not bolted shut. If you are a UK investor whose portfolio overlaps with formal-verification, regulated-sector software, or critical infrastructure, a short note to the email below will be read by the person who would actually decide.

We will not be returning calls from anyone who frames their interest as "moving fast on AI" without engaging with the verification piece, because that is the part that distinguishes us from the rest of the AI-coding category. The verification is the moat.

The investor relations department

Is the same person as the engineering department, the operations department, and the cleaner. Email reaches him.

Tony Gair — founder
tony.gair@thedarkfactory.co.uk
The Dark Factory Ltd · Companies House No. 17050402
South Shields, England