Certified Minecraft redstone

redstone-verify takes a redstone layout and a Verilog spec. It accepts the layout only if it is proved equal to the spec for every input, the proof is checked by independent programs, and the layout behaves the same on two MCHPRS engines. AI agents or search may propose layouts. The funnel decides.

Browse all 92 layouts. Each has a card with its verdict, and 92 of them open in a viewer where you can flip levers and watch the signal.

Read the paper (PDF) · Source code on GitHub

The funnel

A layout is ACCEPTED only if all eight stages pass. The rejection counts are from the shipped mutants: broken copies of accepted layouts, all of which must be rejected.

1. extract

The layout is built as a world and turned into a component graph. Unbuildable layouts are rejected: floating wires, torches without a block, duplicate port names.

2. subset

The graph must use only components with a frozen meaning: levers, wires, torches, repeaters, comparators, lamps, constants. No feedback loops.

3. ports

The spec's ports are 1-bit and match the layout's levers (inputs) and lamps or observed blocks (outputs) by name.

4. prove

The graph is turned into Verilog and compared with the spec by a miter. The solver must show that no input separates them.

5. certify

The same claim is redone from an unoptimised AIGER file with a plain CNF encoder. CaDiCaL writes an LRAT proof; rup_check, lrat-check and the verified cake_lpr must all accept it.

6. lean

An independent route: the spec and the layout become Lean definitions and a Lean theorem says they implement each other.

7. cosim

The layout runs on the MCHPRS engine and on redpiler. Both must equal the model and the spec: every input up to 16 inputs, else structured plus 4,096 random vectors.

8. metrics

Blocks, volume, components, critical path, settle ticks and glitches are recorded.

Benchmark

25 circuits from a NOT gate to a 15-bit adder, a 16-bit comparator and a multiplier. Blocks count every block including levers, lamps and floor. "Best" is the smallest accepted candidate in this table (hand-designed, agent and hill-climb candidates); a later ShinkaEvolve search found a 10-block AND that is not listed here. Time is prove plus certify of the best layout, from one run on an idle AWS server. Mutants: rejected / shipped, and in parentheses how many of the rejected still pass co-simulation. Components, critical path and glitches are seed/best. Click a circuit to see its layouts.

Viewer

The viewer covers layouts up to 1,000 blocks. It has an isometric and a plan view with a layer slider. Clicking a lever flips its input.

Additional experiments

Multipliers: proof search and proof checking

A separate three-seed campaign extends certificate measurements: at 22 inputs, median CaDiCaL time is 1825 s against a*b, versus 10.4 s against the layout's array architecture. Checker time scales approximately with LRAT size (empirical log-log slopes 0.86–1.00), while proof search and size grow sharply across architectures. Bit-parallel enumeration is faster throughout the measured 10–22-input cross-architecture range, but yields no checked proof. These are certificate-route results, not full-gate ACCEPTs; timings use a shared host.

Weak carry chains: faults missed by generic tests

A separate carry-skip adder experiment exposes faults missed by the tests. At widths 12–14, 20 of 45 faulty layouts pass the gate's co-simulation and both generic structured suites. The proof refutes all 45, with counterexamples confirmed on the engine; all 6 fault-free controls receive full ACCEPT. ABC also finds every fault, as do a fault-specific structured suite and 10⁶ random model vectors. At widths 15–24, 10⁷ random model vectors miss 3 of 24 faults; above 15 bits the engine's 32-input limit prevents replay and full ACCEPT.

Independent encoding and mutation checks

A separately written Rust encoder agrees on 62 accepted and 116 refuted miters, with all 62 independent UNSAT certificates checked by cake_lpr. Translator mutation tests exercise 314 single-site and 10 paired faults, with no observed false ACCEPT: 227 are detected (20 only by differential regressions outside the gate), 68 change no layout of the test pool, and 29 are noticed by nothing. A separate wire/timing generator produces 748 mutants, including 510 proof refutations and 224 steady-state equivalences; co-simulation misses 4 refuted wide-layout mutants.

Third-party compilers

We imported layouts from three public redstone compilers and ran them through the same funnel. 504 layouts were imported and 470 were accepted. 99 came from a compiler run and 65 of those were accepted. The rest are the compilers' own shipped example files. Every rejection has a located cause.

Findings in the compilers' output

Reproducers have been reported to Redstone-Compiler, REDA and MCHPRS. The separate certificate-checker finding is reported to drat-trim.

F1. Redstone-Compiler: input ports that feed back into the logic

In its exported and2 the torch that computes NOT a powers a block that touches a's own input wire. That is a one-torch ring oscillator. Source inspection suggests that candidate testing with levers, followed by export with wire at the ports, explains the discrepancy; we have not instrumented that execution path. With levers at the port cells the same world is accepted with a certificate.

We placed the raw layouts in vanilla Minecraft 1.21.1. The ring runs with period 4 for eight pulses, then the torch burns out and the ring stays dead. So vanilla does not oscillate forever, but the world is still not a working gate: nand2 gives the wrong output at a=0, b=1, and and2 matches its table only after the burnout. The tool's own simulator calls and2 wrong at a=0, b=1 (y=1, spec 0).

F3. REDA: redstone dust with nothing to stand on

REDA places dust on top of dust (xor2, xnor2) or on a repeater (or17). Its own simulator calls these layouts correct. Vanilla removes that dust when the layout is placed. The outputs then equal the dust-removed engine variant on every probed vector and differ from the spec exactly where the proof says: xor2 gives y=1 and xnor2 gives y=0 at a=b=0, and or17 gives y=0 with only i15 or only i16 on. For or17 all 4,096 random co-simulation vectors pass. Only the proof finds the bug.

Also found: Redstone-Compiler's interface.json lacks the placement offset and the outputs (F2). rtl2mc uses a redstone block that is outside our subset (F4). Redstone-Compiler cannot compile most of the benchmark (F5).

What this does not show

• The proof is about steady state. Timing, glitches and torch burnout are outside it. Glitches are measured, not proved.
• Only combinational layouts are in the subset. Latches and clocks are not.
• The vanilla Minecraft oracle is a spot check on a sample of vectors, not a proof.