Live project · started August 2026 · updated 26 August 2026

Multics, converted in public

Multics is the 1960s operating system Unix was the reaction to — a quarter of a million lines of PL/I, long dead, historically priceless, and harmlessly public. We are converting its modules into formally proven SPARK Ada, in the open: every number on this page is re-derivable, every difficulty is labelled, and the classes we count against ourselves are listed first.

Recount in progress — 84 of a pinned 219 classified

The conversion line runs continuously, so any count of it is a count at a moment. This recount is against a snapshot of 219 modules taken at 05:00 on 4 September 2026 — every module that had converted Ada through flow analysis at that instant. The line has produced more since and will produce more again; those are not in these figures and will be recounted in their turn. The classification is not finished: 84 of the 219 are done, so what follows is a sample and it will move.

An earlier version of this section gave two different corpus figures in adjacent paragraphs, taken from two different measurements minutes apart. On this page of all pages that is not acceptable, and it is corrected here rather than quietly edited away.

The number worth taking from this page: of the 84 classified so far, 1 is proven. Compiling is not proving, and the gap between those two figures is the entire reason this page exists. Across the 84, 7,079 runtime checks were analysed and 1,586 remain undischarged — 22%. That is the honest state of the work, not a target we are approaching.

This paragraph said 2 are proven until 10 September 2026, and gave 6,469 runtime checks with 1,528 undischarged. Both were wrong. bce_console_io was listed as PROVEN on the strength of its contract and runtime-check columns, which are indeed clean; its summary table carries 55 obligations in total and 2 of them are undischarged, so the classifier makes it PARTIAL. The runtime figures matched no state of the underlying rows, which sum to 7,079 and 1,586. Corrected here, in the open, rather than quietly edited away — and the correction moves the headline number down.

The last completed classification — 153 modules through the prover

One more honesty note, and it is against us twice. The tool that reads the prover’s output was found defective on 21 August (it under-read failures); it was fixed and a regression test pins that fix. On 24 August it was corrected a second time: MEMSAFE had been awarded to modules that still carried undischarged runtime checks, when the label should require that count to be zero. The recount moved 92 modules from MEMSAFE to UNPROVED — not one of them was clean, and the worst had 81% of its obligations undischarged. No proof was re-run and no measurement changed; the underlying rows were always sound. Only the labels were wrong, and this page carried the wrong ones until 3 September. The totals are unchanged at 153, and PROVEN has been 5 throughout. A checker that flatters you is worse than no checker — including when it flatters you twice.

Two cohorts, never pooled

The corpus is split deliberately. The MRDS cohort — 503 database-internals modules averaging ~600 lines — is the credibility cohort: nobody can dismiss a result taken from 950-line database packages. The small cohort — 120 modules averaging 108 lines — raises the proven count and clears the oracle’s wall. Results are reported per cohort, never combined, because a pooled average would be a cherry-pick with extra steps.

The oracle: the original, running

A proof says the Ada meets its contract. To check the contract captures Multics, we run the original: MR12.6f boots under the dps8m simulator on our own hardware, and original modules and their Ada twins are run on identical inputs and diffed. That campaign is live and honestly stuck at its first wall — see below.

Where the difficulty actually is — labelled

• The external-call wall. Most Multics modules call other Multics (family_$entry style). A twin whose externals are unbound stubs cannot run under the oracle at all — this blocked 8 of the first 13 oracle candidates and is the single biggest obstacle.
• MRDS database internals. 950-line PL/I packages with heavy pointer and structure use — the hardest translation targets in the corpus, kept in the count precisely because they are hard.
• PL/I idioms without Ada equivalents. Fixed-point decimal habits, based variables, condition handling — each needs a proven-equivalent idiom, not a transliteration.
• Toolchain failure classes. Our own pipeline stages fail in named ways (resolver failures, expander failures) and those failures are recorded per module, not retried into silence.
• Vacuity. The subtlest failure: a discharged proof that proves nothing. Detecting it is part of the method; the 8 above are its current score.

Why the rest failed — five families, read from every failed attempt

On 4 September we stopped estimating why modules fail conversion and read every failed attempt instead, 332 modules’ worth. The failures are not mysterious. They are ordinary compile errors, and they sort into five families.

Ranked by modules affected, not by error count. Raw counts mislead: one bad name derails a parse and the rest of the file reports as noise.

Three of the five are legacy-dialect carry-through and need no cleverness at all, only a source transform before conversion begins. That is nearly forty percent of the failing modules. The library family is the one that will take time, and we have not yet ruled out that part of it is an environment fault rather than a translation fault; we say so rather than assume.

What this does not change: none of the counts above. The 219, the 84, the 1 proven stand as they are. This section is about why the rest failed, which is the thing worth knowing.

Why publish it like this

Because this is the report format we want to be held to. A dead operating system can be worked on with zero disclosure risk, so it is the right place to set the standard in public: real counts, defined classes, difficulties named, instruments audited. When we publish results about software that is alive, this is the shape they will arrive in.

Back this conversion

Multics is the first publicly backed project of the member economy: members will be able to donate credits from their account straight to this conversion, and card backing will top an empty balance up on the spot. That rail is being built — and in keeping with this page’s rules, the button below does only what is real today: it opens a pledge, we record it, and nobody is charged anything until the rail is live and you say so again.

PLEDGE BACKING →

The wider project this belongs to — a private assistant whose every decision passes proved rules, and the research group forming around it — lives at thereef.ink.