> For the complete documentation index, see [llms.txt](https://docs.moduluszk.io/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://docs.moduluszk.io/the-problem/what-removal-looks-like.md).

# What removal looks like

Removing the gap means having one artifact. The rule a human writes must be, literally and byte for byte, the thing the chain enforces. That requires the chain to enforce logic directly: no compilation into an executable form the author never reads, no machine whose behaviour stands in for the author's meaning. A transition is admitted when the stated conditions are proved to hold over it, and refused otherwise. 

That is what Modulus is. The next two pages describe the mechanism: what a predicate is and why it occupies the slot a contract occupies, and how proofs admit state transitions.