Heuristics Propose, Certificates Decide: A Fail-Closed CTL Compiler for Petri Nets

Learned and hand-written heuristics can make symbolic reasoning useful, but they should not authorize an answer. We introduce source-licensed symbolic compilation: a source witness licenses a closed set of rewrites, a producer emits a source-bound proof DAG, and a separate replay checker either reconstructs the claimed judgment or rejects it. The producer may use learned scheduling; the checker never does. Our concrete system is a partial CTL compiler for ordinary Petri nets. It combines local rules, exact P-invariant/Farkas leaves, and a fixed-token state-machine specialization with formula-labelled quotients. On 464 Diffusion2D queries it returns 263 Booleans, all replayed by the checker. Across five fixed representative ranks, portable licenses decide 470/7,504 queries from 93 MCC families, while the specialized license remains narrow. A sealed temporal test of source-only SAT proof scheduling retains every certifiable instance but does not beat the best static order, failing six of nine preregistered gates. Across three fixed-order runs of the largest NeighborGrid model, a two-pass constructor reduces median producer peak memory from 15.19 to 0.650 GiB without changing base coverage; quotienting then closes two budget-exhausted queries. The result is a checked boundary for fallible search: learning may choose what to try, but only source-bound certificates authorize a verdict.