EXECUTION IS EVIDENCE: CERTIFIED SEMANTIC PROGRAM IDENTIFICATION

A program can be identified by what it does even when its source syntax is unrecoverable. We study semantic program identification from partial executions with independently checkable correctness. First, a routing-and-witness condition gives an exact family with d + r adaptive versus d + 2d r fixed queries, and a separate nonlinear repeated-operator language admits exact worst-case optima 6 < 9, certified by a complete decision tree and an independently checked adversary DAG over all 10,974 behaviors. Second, for a fixed accumulator language we prove a width cutoff: two programs of length at most L agree at all bit widths iff they agree at width 2L + 1. This turns large-width uniqueness into a cutoff-width symbolic refutation without enumerating the input domain or the behavioral quotient. On eight adapted 32-bit Hacker’s Delight specifications, all 120 paired runs return independently checked programs. With the same cutoff reduction, adaptive witness queries use 3.125 replies and 0.304 seconds on average versus 4.375 replies and 0.335 seconds for structured fixed probes; holding the word and transcript fixed isolates a 4.47× reduction in terminal certification time. Under the same per-call conflict budget, the cutoff also raises horizon-six certification coverage from 1/8 at native width to 8/8. Together, the results connect adaptive observation design with proof-carrying semantic identification under explicit, executable contracts.