arXiv:2610.27805v1 Announce Type: new Abstract: Maximum-likelihood (ML) decoding of linear block codes is NP-hard, so neural decoders are evaluated by how closely they approach it. We observe that proving a candidate optimal can be far easier than finding it, and build a decoder that does both. We cast decoding as a search over an absorbing-state discrete diffusion model, whose sequential commitment of coordinates turns generation into a tree, and run a probability beam search over it. A dual bound from a linear-programming relaxation and a distance-based test, both derived from the code, then certify per frame that the current candidate is the global ML solution; because both are theorems, certified frames incur no accuracy-computation trade-off. Across $15$ codes and five operating points we certify up to $99.9\%$ of frames, the two tests dividing the space as their derivations predict, one strong for sparse parity-check matrices and the other for codes with a large minimum distance. Certification also behaves as a per-frame reliability signal, with $96.7$-$100\%$ of all frame errors falling on uncertified frames. Against an exact ML reference at $5$ dB the decoder is within one standard deviation on three of the four codes where the reference is uncensored, and against four neural baselines it attains the best bit-error rate in $71$ of $75$ cells.