What is Equivalence checking? Definition and why it matters
===========================================================

Proving that two artifacts compute the same function, for example optimised assembly against a Cryptol reference, or the KEVM semantics against a Lean EVM model.

Detail: Equivalence checking is how existing optimised code gets verified without rewriting it. Its limit is that the reference must itself be trusted or verified.

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