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?

i'm a long time lisper, but i don't think this is justified.

implementing prolog/backtracking on top of lisp is certainly possible and not even too hard (see e.g. https://github.com/nikodemus/screamer)

and implementing Coq on top of lisp is also possible.

but IMO the "with ease" phrase is not justified in this context.

if you only mean that lisp will not be in the way if you set out to implement these, then i agree. lisp -- the language and the typical opensource implementation -- will be much less of an obstacle than other languages when chosen as foundations.

You can write a prover like Coq in a Lisp, but, though it's easier than doing it in C, I think it's somewhat harder than doing it in something like OCaml. ACL2 is an example of such a thing.