The Refutation Gap: Certifying Both Halves of an Optimality Claim

Rohan Pandey

Synthesis pipelines increasingly claim not just that a program is correct, but that it is optimal. Such a claim has two halves with radically different verification stories. The up…