In an era where we’re dependent on software to the extent that it can compromise our safety and health, programs must provide guarantees that they meet their specifications. In many cases, testing and other non-mathematical techniques do not provide strong enough guarantees, so we have to resolve to formal reasoning. Formal reasoning is the practice of formally proving that a program meets its specification. Our work focuses on theorem-proving: an approach to formal reasoning where 1) important/critical properties of the system are specified then 2) a theorem-prover is used to prove that these specifications are met. Reasoning in this way requires a theorem prover, and “reimplementing” the code in those tools can be far from trivial. As a result, proofs about code are done on small parts or simplifications of the original code, when done at all.
