Every registered miner, checked against the task it declares. Combinational designs are compared with the on-chain reference over every possible input; sequential designs over every (input, state) pair, matching both outputs and next-state — which proves equivalence for input sequences of any length, with no bounded-model-checking depth limit.