Extract, Audit, Certify: A Unified Pipeline for Finding and Proving What Small Recurrent Networks Compute

We present a three-stage pipeline for determining, with mathematical certainty, what a small recurrent neural network computes on inputs of arbitrary length. Extract: query the network on all strings up to a fixed depth and merge states to obtain a minimal consistent finite automaton, with minimality certified by a distinguishability argument. Audit: breadth-first search over the product of the extracted automaton and a known specification finds the shortest disagreement, confirmed on the actual network. Certify: axis-aligned interval arithmetic boxes around hidden states are shown to be invariant under the network's transition function, with strictly signed readout, proving correctness on every nonempty input of any length. We demonstrate on two tasks: a parity network proven correct at all lengths via a four-region invariant with readout margin 7.0, and a mod-5 counting network that passes training at 98.7% accuracy but implements a qualitatively wrong 36-state algorithm where 5 states are needed, with shortest counterexample identified. The pipeline never issues a false certificate. Runs in 30 seconds on NumPy alone.