TheReefink

an amateur research group for deterministic, machine-proved extensions to local AI assistants · ghillie, the claw itself →

We are going to safely mutate our claws — deterministically — and build tools that extend their reach, with proved code. An amateur research group, in the radio-ham sense: our own machines, our own proofs, nothing that asks to be trusted. Why organisation beats brain size →

Humans say what they want.

Claws serve.

Claws decide how to change, and cooperate to do it.

Experimentation reveals results.

All benefit, and all provide processing.

The three rules

  1. Nothing asks for trust. Every claim a member relies on must be one they could re-derive: a proof, a digest, a truth table. “The maintainer says so” is not a category we use.
  2. Refusals are findings. A proof that fails to discharge, a store that cannot be read, a gap honestly recorded — these are the system working, and they are written down, never smoothed over. The boring report — it did exactly what its theorems said, again — is a finding too.
  3. The owner outranks the claw, always. Extensions decide; they never acquire authority. No experiment changes that, whatever it would prove.

Become part of it — re-derive your first proof today

You need no account, no registration, and nothing from us you cannot check. New to this? Start with the beginner's path — three steps, nothing installed on your system, and it stops at the proof. What follows here is the full route. Two downloads and ten minutes:

1. Get the prover. The free GNAT FSF toolchain — it carries the SPARK prover and the build tools in one package:

https://github.com/alire-project/GNAT-FSF-builds/releases
  (gnatprove-x86_64-linux, -darwin, or -windows64 — unpack anywhere)

That package alone is enough for step 3, re-deriving the proof. It is not enough for step 4, building the front: it ships gcc and ld but no C runtime and no startup objects, so on a machine that lacks them the build fails after the proof has already discharged — the worst possible moment to find a part missing. You also need binutils and libc6-dev. These are the ordinary build essentials of any Linux system, present already on almost any machine used for development; it is a bare container or a fresh minimal install that goes without. On Debian and Ubuntu:

sudo apt-get install binutils libc6-dev
# Fedora/RHEL: the equivalents are binutils and glibc-devel

2. Get the starter extension. A real decision core — the brief-fill policy, deciding when an assistant may answer on its owner's behalf — delivered as source with its proof and its full truth table:

brief-fill-policy.tar.gz (6,918 bytes)
sha256: 14bb06671459784d2d571e7b5e2afc3037894c241517612b026dbe053fb6b180

That is the same file, at the same address, that the catalogue index names and your ghillie checks — one artefact, so this page and the machine cannot disagree. The whole shelf is at the catalogue.

3. Re-derive the proof. From the unpacked bundle:

cd brief-fill-policy/core/src
gnatprove -P proof.gpr -f -U --level=2
# success: "0 unproved" — four named theorems, discharged on YOUR machine:
#   NEVER-FILLED-WITHOUT-A-LICENSING-RULE
#   AN-ABSENT-STORE-NEVER-LETS-A-FILL-THROUGH
#   NOTHING-INVENTED-EVER
#   NOTHING-ASKED-THAT-A-RULE-ALREADY-ANSWERS

4. Try to break it. Edit the source so an absent rule store lets an answer through, and run the prover again. It will refuse — naming the exact theorem you betrayed. That refusal is the whole security model, and you just watched it work without trusting anyone. Then build the front and check every row of its shipped truth table (core/REPROVE.md in the bundle walks you through it).

The aim

To reach the position where our cleverness and cooperation make our tokens and our reasoning the best available — and every member effectively super rich. Rich in the currency that matters here: proven reasoning compounds like a library, not like a pie — every core added makes every member wealthier at nobody's expense, until an ordinary member's claw commands more checkable capability than money can rent.

Why the work is named Wu

The factory's unit of work — one proved rule, forged from a plain sentence — is called a Wu, after Chien-Shiung Wu.

In 1956, Chen-Ning Yang and Tsung-Dao Lee asked a magnificent question — does nature tell left from right? — that nearly everyone thought not worth asking. It was Wu's experiment — her design, her rig, her measurement — that answered it. The Nobel Prize, the following year, went to the theorists alone. The question deserved its prize; so did the answer, and the answer was left out.

Both halves of that story live here. The bold question, plainly asked, is where every piece of our work begins — we honour Yang, and we emulate him. But we name the unit of work after Wu, because the proof is the work: not the idea, not the announcement — the demonstrated, checkable result. And we name it after her in public because we know how easily the person who does the demonstrating gets erased, and it will not happen here.

What is coming

Reports

Ran the proof? Broke something politely? Found the boring result? Write to reefink@thereef.ink. Findings are published; nothing else about you is asked for — this page has no scripts, no cookies, and no analytics, which you can check by reading it. The server that hands you the page does keep one short, truncated line per request, and says so plainly: what the server records.

Patronage

TheReefink is patroned by The Dark Factory Ltd, which has devoted considerable resources to its success — the proving machinery, the first extensions, and the terminal to come. The patronage buys no exceptions: everything the patron ships here is checkable by the same rule as everything else, and a member who breaks it politely has done the group a service.