Machine code in. Formulae out. Solver next. The syntax-to-semantics bridge, made mechanical — within a bound.
Run it on some inputs. Shows presence, not absence. One point per run in a space of 234,359,738,368.
Decides everything about the text, nothing about behaviour. A warning is a question about the text in disguise.
For every input, for every path, up to k steps: can the program reach a bad state? A yes comes with the input. A no is a theorem — up to k.
Rice said: choose what to give up. Today we give up everything beyond step k, and get, in exchange, absence.
Week 3: addition is a circuit of gates. A gate is a formula over bits: and, or, not. So a 64-bit word is 64 variables, and every instruction of week 6 — add, compare, load, branch — is a formula over the bits of its registers.
One step of the machine is one big formula: the new state in terms of the old, depending on which instruction the pc points at. That is what Cook's proof did to prove SAT hard. Here it is a tool.
Solvers that speak words and memory, not just bits: the theory of bitvectors, the theory of arrays. Underneath, they bit-blast to the SAT of last week and run the same clever search. Z3 and Bitwuzla are two of them.
Reads one byte. Subtracts 48, the code of the digit 0. Divides by the result. Type 0 and it divides by zero; type 1 and it exits with 1; type 2 and it divides by zero on the other line; type anything else and it exits with 0.
Rotor compiles the program with selfie's compiler and writes the model of the RISC-V machine running that binary: every instruction, bit-precisely, as a formula. Linear in the size of the code — it does the same to all of selfie.
States: the pc, the registers, the memory segments, and an input buffer left uninitialised so the solver may choose it. Init: what they are at step 0. Next: what they are one step later — the RISC-V semantics. Bad: twenty-four things the machine must not do.
Bitme walks the steps one at a time and asks about every bad state at each. For the first few dozen the answer is no: the program is setting up its stack, calling malloc, calling read. Then the division instruction is fetched, and the answer for division by zero is yes — with the input that does it, derived from the formula.
Among all 256 possible input bytes, the solver found the one that reaches the bad state, the way last week's solver found that x1 must be false: not by trying them, by reasoning. And it did it for a compiled RISC-V binary, not for the C.
Visits one state per run. Shows presence. Says nothing about the inputs you did not try.
Every input, every path, up to k steps. Shows absence, within the bound. Says nothing beyond it.
Rice said no tool decides whether a program can divide by zero, and this one does not. It decides whether a program can divide by zero within k steps, which is a question about a finite object and therefore decidable — and it pays for the answer in solver time that grows with k. Choosing k is choosing what to give up.
That is formal methods in one sentence, and the workshop around selfie is a set of such choices, each stated: rotor, bitme, babysat, a fuzzer, a second garbage collector, a binary translator — each applied to selfie, and to itself.
Take a program, which is syntax, and its execution, which is semantics, and produce a formula whose satisfiability answers a semantic question exactly — within a bound. The formula goes to a solver, and satisfiability is the canonical hard problem.
So a laptop, a small C program and twenty minutes get you to the frontier of complexity theory. That is not a metaphor. It is what just happened on this screen.
A machine that produces programs, fluently. The one thing it cannot supply is the check you just watched. Bring the gate.
Machines: what a large language model mechanically is, why a hallucination is a proof-shaped object that is not true, and the gate that the machine cannot supply.