Can We Verify What a Code Model Tracks? Syntax, Binding, and Procedure Along Transformer Trajectories

A code model can produce the right answer while leaving open a harder question: what did it preserve internally to get there? Verification at the output cannot distinguish syntax, binding, procedure, and result if they are collapsed into one final success label. Extending a trajectory-based bounded-interpreter framework, we define code interpretation as a structured state over syntax, binding, and procedure, and ask whether successful code continuation leaves measurable evidence of those constraints in transformer hidden and logit trajectories. In a controlled synthetic code language, a small transformer recovers syntactic validity, branch-dependent binding, procedural condition, and final result with perfect held-out accuracy; local Jacobian analysis shows roughly 5.5 times greater sensitivity to semantically relevant code tokens than to structural filler; and a 24-dimensional lifted representation explains 98.2