Can you give an example? With something like Figure 1 of the paper converted to a convenient form for Lisp (s-expressions, presumedly), and assuming a function to convert it to binary, what would it look like to prove correctness of that assembly in Lisp? What's the ecosystem of proof assistants that would get you there?