Refinement
Direct answerA 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.
In more 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.
Related terms
Circuit soundness, Circuit completeness, Underconstrained circuit, Overconstrained circuit, Symbolic vs computational model, Specification gap, Trusted computing base and verification boundary, Proof assistant vs SMT-based verifier, Bounded model checking, Equivalence checking, Constant-time verification, Arithmetization (R1CS, PLONKish, AIR), Extraction (code to model), Witness generation vs constraints
Getting help
Firms on this index that handle this in practice: zkSecurity, Galois, Veridise, Nethermind (Formal Verification team).