Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete
J Moore (but presented by Matt Kaufmann)
ACL2 Seminar, 5/16/2024

Abstract (quoting the paper, to appear in ITP 2014):

In this paper we sketch an ACL2-checked proof that a simple but
unbounded Von Neumann machine model is Turing Complete, i.e., can do
anything a Turing machine can do. The project formally revisits the
roots of computer science. It requires re-familiarizing oneself with
the definitive model of computation from the 1930s, dealing with a
simple “modern” machine model, thinking carefully about the formal
statement of an important theorem and the specification of both total
and partial programs, writing a verifying compiler, including
implementing an X86-like call/return protocol and implementing
computed jumps, codifying a code proof strategy, and a little
“creative” reasoning about the non-termination of two machines.