Before revision: A theorem prover or certifying compiler is used to show that the machine code satisfies this policy.
After revision: A theorem prover is used to show that the machine code satisfies this policy.