Proving a Trained Network Is a Finite-State Machine: an Exact Certificate, Its Witness and Its Numerics

The problem. A network trained on a task that a finite-state machine solves can pass every test and still be wrong: tests sample, and a machine extracted from the network is not the network. This note decides exactly whether such a network computes the same function as a given machine, on every input of every length it can read. Why it matters. Claims that a network learned a rule, networks standing in for programs, and the search for unknown machines from behaviour all need that answer and mostly estimate it. The method needs a design: when the only channel between a recurrent network's steps is a finite code, each state replaced exactly by its nearest codebook row, the network is a Mealy machine, and equivalence is decided by enumerating every reachable code under every input window. That core has a recent precedent (Brandoit et al. 2026). This note states it as a method for steps that read the state, with its proof, near ties branched, a witness that an independent checker verifies by re-running every entry through the forward pass, and sound interval and affine bounds on its floating-point decisions. Validation, on existing networks with none trained: all 1,077 certified tables of 674 networks valid and all 11 uncertified ones invalid; a modelled sampled test misses a planted fault at a rarely visited entry with chance up to 0.9998 on modular division; every entry's decisions in the 613 tables the bounds cover hold for the network's real-valued function. Without the target, the proof needs a bound on the target's size. How this work was done. David Barkhuizen posed the question this note serves, learning finite-state machines from their behaviour and known structure, with proof; asked for this note and its framing; and decided what it claims and how it is published. Claude (Opus 5.5, a model made by Anthropic), working through Claude Code, did the rest: the literature review, the witness, the checker, the fault injection and the bounds, their runs and analysis, and the drafting. Claude is not listed as a creator because it cannot be accountable for the record; this note says who did what. Not yet independently checked. This is a preprint, not peer reviewed. It was reviewed against the data, the reasoning and the literature by fresh instances of the same model; no one outside this collaboration has checked it. A fault found will be corrected in a new version, or its claim withdrawn. Anthropic as an organisation has not been involved in this work and has not consented to, reviewed or endorsed it.