A core is a small unit of SPARK Ada whose contracts the prover has discharged at level 2 and which a second machine has proved again from the same source. The count is of distinct cores in that record, not lines of code. The Multics and physics figures are explained below.
Portfolio · Reference Outputs
These are reference outputs of the Dark Factory's SPARK-Ada production line — packages generated from prose specifications and legacy source code. Each is included because it demonstrates a distinct dimension of what the factory does: legacy modernisation, domain-specific calculation, or formal-method substrate over a real prose specification. The ledger lists everything, including the conversion we cannot finish. A supplier who shows you only the work that went well has told you nothing you can use.
None of these is a customer engagement. The factory has no paying customers yet. Everything on this page was chosen and built by us, against sources we picked ourselves — public codebases, published specifications, our own briefs. That is worth knowing before you read the results: nobody external set the problem, and nobody external has yet had to live with the answer. Case studies with a client's name on them will appear here when there are any, and not before.
Not all of this is published yet. Where we start from someone else's source we keep to its licence, including copyleft ones.
The factory's reusable catalogue components (the building blocks the production line composes against — money types, JSON parsers, vector primitives) are factory-internal and not published here. The portfolio shows the outputs, not the production machinery.
Current work
We'll rebuild any system you commission, whatever it's written in. These are the ones we've done ourselves, on public code. Nobody paid for any of them.
Vincent Coen started writing ACAS in 1976 and still maintains it. We rebuilt parts of its sales ledger reporting in SPARK Ada and ran them against what his system actually printed. Six of them were compared that way and agreed on every case we tested. It runs on this site, with his blessing.
Agreeing isn't the same as covering everything. Some cases weren't tested and we say which. ACAS flies again.
We converted 219 modules of Multics PL/I to SPARK Ada and put every one of them through the prover. Most of them don't prove. We publish the counts as they stand, including the ones that went down when we measured again.
Proven protocol software for the systems that run water, energy and transport, with a gateway in front of the plant.
The gateway. A proven command gateway for industrial controllers, demonstrated end to end against a simulated controller. The parts that move bytes on and off the network are tested, not proved.
The protocol software. Proven where it reads messages and where it decides what gets through.
None of it is certified. Cyber-harden.
Two one-dimensional finite-volume schemes, linear advection and inviscid Burgers, rebuilt in SPARK Ada and proved against IEEE 754 double-precision arithmetic as executed, not over the real numbers. Where an identity holds exactly in floating point it is proved exactly. Where rounding makes that impossible, it is proved within a stated bound (the wave-jump condition to within 6 units of roundoff, the conservative flux to within 10). Division by zero at zero wave speed is ruled out by a stated precondition, and the Burgers sonic point is defined rather than left to chance.
Why it matters: a proof over the reals says nothing about NaN, overflow or rounding in the code that actually runs. Run side by side with the original generated C on about 252,000 inputs, the only differences were zero-speed cases where the C returns NaN and ours refuses the input by name.
Our first runs were on public Fortran and one benchmark: DL_POLY Classic, LAPACK's DGESVD, the USGS seismic hazard code, the DTU wind turbine controller, and a UK income tax calculator. They produced Ada with contracts, but the bodies were incomplete and none of it was proved, so we've stopped describing them as finished work. They're still in the ledger below.
Production Ledger · Full Manifest
Everything we've put through the factory, including the work that didn't come out well. The Fortran rows are our first runs, from May and June 2026. They compiled, but the bodies were incomplete and none was proved, so they carry no proof figure.
| Source file | Project | Origin | LoC | Pkgs | Status |
|---|---|---|---|---|---|
| ACAS — Applewood Computers Accounting System · 275 programs · COBOL, 1976– · running on this site | |||||
| ACAS (275 programs) | ACAS | Vincent B. Coen (UK) | — | — | LIVEtwin agrees 21/21 |
| Multics · 219 modules in the pinned snapshot · PL/I · the honest counts | |||||
| Multics (219 modules) | Multics | Bull HN → MIT | — | 219 | CANNOT FINISH6 proven of 219, 3 substantive (one is a struck no-op) |
| Earlier work, May and June 2026 — not proved · Fortran · compiled, bodies incomplete | |||||
| DL_POLY Classic · 22 modules · 54,880 LoC | |||||
| DL_POLY Classic (22 modules) | DL_POLY Classic | STFC Daresbury (UK) | 54,880 | 109 | EARLIERnot proved |
| USGS NSHMP · 3 sources · 3,997 LoC | |||||
| hazSUBX.f | USGS NSHMP | US Federal (Golden CO) | 3,698 | 11 | EARLIERpartial: 89.9% of checks proved |
| hazpoint.f | USGS NSHMP | US Federal (Golden CO) | 224 | 1 | EARLIERnot proved |
| gutenberg.f | USGS NSHMP | US Federal (Golden CO) | 75 | 1 | EARLIERnot proved |
| European Space Agency · 2 sources · 6,346 LoC | |||||
| OPTGRA (37 files) | European Space Agency | ESOC Flight Dynamics | 3,760 | 22 | EARLIERnot proved |
| Planck CAMspec (5 files) | European Space Agency | Planck Collaboration | 2,586 | 14 | EARLIERnot proved |
| LAPACK 3.12.1 · 1 source · 3,552 LoC | |||||
| dgesvd.f | LAPACK 3.12.1 | UT + UC Berkeley | 3,552 | 4 | EARLIERnot proved |
| DTU Wind Energy · 1 source · 1,291 LoC | |||||
| dtu_we_controller.f90 | DTU Wind Energy | DTU (Denmark) | 1,291 | 5 | EARLIERnot proved |
| Earlier Fortran work (29 sources, 5 institutions) | 70,066 | 167 | not proved | ||
Open Source · Ada Ecosystem
Alongside the verified conversions above, the factory publishes open-source Ada bindings to
widely-used C libraries, filling gaps in the Ada / Alire ecosystem. These are bindings,
not formal conversions — listed here on their own terms, kept separate from the proof
tallies above. They live in the
the-dark-factory
organisation under permissive licences, published to the Alire package index as the
df_ crate family (df_vulkan is live on the index; the rest are in review).
A complete Ada binding to Vulkan, with a SPARK-verified safety layer on top: resource-lifecycle misuse — use-after-destroy, or creating a child object from a destroyed parent — becomes a compile-time proof obligation instead of a runtime crash. We are not aware of another Vulkan binding with a machine-checked safety layer.
Ada bindings to Liu Liu's CCV, a modern C computer-vision library — image input / output and processing, callable from Ada.
Ada bindings to the STB header-only C libraries — image load / write, TrueType font rasterisation, and more, from Ada.
Ada bindings to Dear ImGui, the immediate-mode GUI toolkit, via cimgui — debug overlays and tooling UIs, from Ada.
Ada binding to Box2D v3, the widely-used 2D rigid-body physics engine — bodies, joints, and collision, callable from Ada.
Ada bindings to llama.cpp — run a large language model on-device,
from Ada, no cloud required. A companion examples crate
(df_llama_examples) includes a live token-confidence visualisation:
watch how sure the model is of each word as it speaks.
How To Engage
We'll rebuild any system you commission, whatever it's written in. C, COBOL, PL/I and Fortran are what we've done so far, not the limit. Tell us what it is and roughly how big; a repository link or a plain description is enough. How a migration runs.