What is Refinement? Definition and why it matters
=================================================

A relation showing that an implementation's behaviours are a subset of a more abstract specification's behaviours, layered so low-level code refines a high-level model.

Detail: Refinement is the methodology of seL4, AutoCorres2 and Apple's corecrypto proofs, and of Coda's refinement types for circuits. It lets a proof be split into stages that different people can own.

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