&quot;I have this high-level specification of a semaphore lock that the model checker can verify and might even have a proof. How do I now implement this in code?&quot;<p>You do them side by side in a way that looks and behaves similarly. That&#x27;s the traditional route going back to Orange Book A1-class systems. The seL4 work did something similar. Two other routes are: (a) gradually refining abstract spec into something concrete enough for code like B method does; (b) using tools like Coq that support extraction of code from specs. Also look into &quot;abstract state machine&quot; specification, code, generation, and so on. Much work happened under that label in both hardware and software.