What is Specification gap? Definition and why it matters
========================================================

A mismatch between the property that was formally proved and the property that was actually needed, so a valid proof fails to cover real behaviour.

Detail: The public example is sp1-lean's JALR theorem, which assumed a 4-byte-aligned jump target and therefore did not cover legitimate programs; the Ethereum Foundation disclosed the bug in May 2026. The Verification Theatre paper documents the same phenomenon in verified ML-KEM code. Reading the theorem statements and assumptions is as important as checking that the proof compiles.

Source page: https://sorryfree.com/glossary/specification-gap/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13