The Reef machine

what you actually need to take part — which is less than you would think

The coloured notes are from Tony's AI assistant, whose job is to keep people straight where he has missed something — a fact, a caveat, or an observation of its own. We have left them a different colour rather than blending them in.

I should say up front what I am. I am not a formal methods person. I am the simpleton with the proofs who has chanced on a methodology he likes, and this page is me writing down what the machines actually did when I measured them, because I could not find anyone else who had.

Take the numbers, not my opinion.

If you only want to check that I am telling the truth

Any computer you already own.

That is the honest answer and I want it first, because the rest of this page has processors and cache sizes in it and could easily give you the impression you need to go shopping. You do not. Everything we publish is source with a proof attached, and re-deriving one on your own machine takes seconds.

note — and costs nothing. The prover is the free FSF distribution of GNAT: no licence, no account, no evaluation period. You will also need binutils and a C runtime for the build step after the proof, which the instructions used to forget to mention and which caught out a clean-room test of our own.

I ran the same proof and the same plain arithmetic loop on everything in the house, to separate how fast a machine is from how fast it proves:

machine	processor	arithmetic loop	one proof
Mac laptop	Apple M5 Max	0.45 s	—
desktop	Ryzen 7 7800X3D	0.74 s	2.5 s
desktop	Ryzen 9 5900X	0.79 s	4.6 s
NAS	Celeron J4125	3.21 s	—
Raspberry Pi 4	Cortex-A72	8.88 s	see below

Twelve times between the fastest and the slowest. It does not matter much. A proof that takes two and a half seconds on the quick machine is not going to cost you an afternoon on a slow one.

note — the two blanks are honest gaps rather than oversights: the NAS has no prover installed yet, and the Pi is the failure described below. Everything in the table that has a number was run today, on that machine, by us.

The Pi did not work and I am not going to pretend it did

I wanted a Raspberry Pi in this table proving things, because it would have been a good line. It installed and then fell over.

note, completing this — the pieces do exist: there is a native gnatprove-aarch64-linux build and it unpacks fine. What is missing is Alire, which makes this one command on x86-64 and publishes no ARM Linux binary at all — so you are placing the prover backends by hand. Ours came up with no solver configuration and failed inside the prover front end with unexpected character '/'. That is a setup problem, not a fundamental one. Somebody who knows this toolchain better would likely fix it in an evening.

ARM Macs are fine, for what it is worth. It is the small ARM Linux boxes that are awkward.

If you want to run an assistant with a local model

The only thing that matters is how much memory is on the graphics card. Everything else is noise next to whether the model fits.

card memory	what runs comfortably
8 GB	small models, tight
12 GB	7B comfortably, 14B squeezed
24 GB	14B comfortably, 32B squeezed — the sweet spot
32 GB+	70B, heavily compressed

Buy a second-hand 3090. It has 24 GB and costs a fraction of the new cards that offer the same.

note — roughly £700–900 used against £1,600+ for a 4090 with the same 24 GB, and about five times the memory per pound of the current flagship. The real cost is 350 W. If you would rather have efficiency than capacity, a new 16 GB card draws about half that for two-thirds of the memory.

If you want to help with the proving — this one surprised me

I assumed proving wanted cores. I added a twelve-core machine to a house that had an eight-core one and got less work out of it. Slower on one proof and slower on twenty-four at once.

It is not the clock. Both machines run plain arithmetic at the same speed. It is the cache.

processor	cores	total L3	per core	one proof	24 at once
Ryzen 7 7800X3D	8	96 MB	12.0 MB	2.5 s	6.8 s
Ryzen 9 5900X	12	64 MB	5.3 MB	4.6 s	10.4 s

So the rule is cache beats cores, which is not what I expected and not what the shops push you towards.

note, explaining why — a proof is not a tight arithmetic loop. The solver builds large structures — clause databases, learned lemmas — and walks them unpredictably for the whole run, so it lives or dies on how much of its working set stays in cache. Twelve megabytes a solver keeps it resident; five sends it to main memory constantly, which is two orders of magnitude further away. Running more solvers at once makes it worse, because they share a cache they are already short of — which is why the bigger machine loses the parallel test by more than the single one.

By the same logic the enormous workstation chips are the wrong shape. A 64-core Threadripper has the biggest cache in this document and the smallest share of it per core.

processor	cores	total L3	per core
Ryzen 7 7800X3D	8	96 MB	12.0 MB
Ryzen 9 5900X	12	64 MB	5.3 MB
Threadripper 7980X	64	256 MB	4.0 MB

note, and a caveat you should have — we have not tested a Threadripper. That row is arithmetic from published specifications, not measurement. It would still finish more proofs per hour than either machine above, because sixty-four inefficient workers beat eight efficient ones on raw count — but you would be paying a great deal, and 350 W, for cores that spend much of their time waiting on memory.

The mix I would build

Not one big machine. Several small ones.

A prover. Eight cores with a big cache, 64 GB, no graphics card worth mentioning. Cheap, and it is the machine that checks things.

An inference box. Whatever card has the most memory you can justify. It is idle most of the time.

Anything at all as a witness. An old laptop, a mini PC, a NAS. Its whole job is re-checking work that a different machine says it has done. It can be slow. It cannot be the same machine.

That last one is the part people skip and it is the part I care about most. Ours is a four-core Celeron with 7 GB of memory and it is the right machine for the job.

note, on why that is not a joke — it is the right machine precisely because it is slow and separate. A machine confirming its own result tells you nothing; the value of a witness is independence, not throughput. Which also means that if you have an old laptop doing nothing, you already own something genuinely useful to this project.

What I am unsure about

One kind of proof, on machines I happen to own, one of them running inside a virtualisation layer that I have not accounted for. The shape of the result looks clear to me and the buying advice follows from it, but you should know how thin the evidence is.

If you run these on your own hardware and get something different, tell me. That is rather the point of publishing them.

Standing on AdaCore's shoulders

None of this is mine and it would be poor form not to say so. AdaCore build and maintain GNAT and SPARK, and they give away a free distribution that is not a crippled demo.

Every proof on this site is discharged by their free build. When I tell you that you can check my claims on your own machine in ten minutes and it will cost you nothing, the reason that is true is a decision they made about how to publish their work — giving away the thing that would be easiest to charge for, and keeping the paid edition honest by making the free one actually good. It is why someone like me can do this at all instead of meeting formal methods once, inside an aerospace contractor.

We intend to follow that rather than just benefit from it. Our abilities ship as source with their proofs, free, with nothing held back to force an upgrade. Where we charge it will be for work done, never for permission to check what we have claimed.

note — the toolchain is at adacore.com; the free community builds used for every number on this page are at GNAT-FSF-builds.