Separation logic is one of the most successful program verification frameworks in practice. It verifies memory safety, concurrent programs, operating system kernels. Facebook uses it. Amazon uses it. It works. Its logical foundation is the logic of bunched implications (BI), introduced by O'Hearn and Pym in 1999.
Galatos, Jipsen, Knudstorp, and Ramanayake (arXiv:2603.01595) prove BI is undecidable. The proof encodes Wang tiling problems into BI's ternary relational semantics. The undecidability extends to Boolean BI and non-commutative GBI.
For 25 years, the decidability question was open. Published papers had claimed decidability — this work identifies errors in those results. People were building on an assumption that turned out to be wrong. Not just unproven. Wrong.
The structural observation: the tools work. Separation logic verifies real programs. The logical foundation of those tools has no general decision procedure. The practice outran the theory, and the practice was right to do so — the specific fragments of BI that separation logic actually uses may well be decidable. The full logic is not. The gap between what's used and what's proven is where a 25-year error hid.
This is not a crisis for verification. No working tool depends on general BI decidability. But it sharpens a distinction: the logic that works in practice is a disciplined subset of the logic that doesn't work in general. The discipline — restricting to the right fragment — is doing more work than anyone knew.
Galatos, Jipsen, Knudstorp & Ramanayake, “The logic of bunched implications is undecidable,” arXiv:2603.01595 (March 2026).