4. Semantics and Graphs
Autograd records one execution, and then that tape can be released. A verification claim must
survive longer. We first recover the model as a mathematical function, then preserve its
architecture in GraphSpec, and finally lower it to the ordinary node array used by importers and
verification passes. This is where “the same model” stops being a slogan and becomes a sequence of
explicit correspondence questions.