This demo is adapted from these files of J Moore
in the ACL2 Community Books; see them for details.
(I don't do this sort of thing myself!)

https://raw.githubusercontent.com/acl2/acl2/master/books/models/jvm/m5/demo.script
https://raw.githubusercontent.com/acl2/acl2/master/books/models/jvm/m5/jvm-fact-setup.lisp

We consider this class:

class Demo {
  public static int fact(int n){
      if (n>0)
        {return n*fact(n-1);}
      else return 1;
    }

    /* This main method is not translated by jvm2acl2 */
    /* because our M5 model does not support the */
    /* native methods necessary to support IO. */

  public static void main(String[] args){
      int n = Integer.parseInt(args[0], 10);
      System.out.println(fact(n));
      return;
    }
}

We include definitions of a JVM interpreter and of
the "fact" method translated mechanically to ACL2.

(include-book "models/jvm/m5/jvm-fact-setup" :dir :system)

Our demo function runs that JVM interpreter for n
steps on a suitably initialized state.

(in-package "M5")

(defun demo-fact (n)
  (let ((sched (fact-sched 0 n)))
    (list (list 'steps (len sched))
          (list 'ans 
                 (top
                  (stack
                   (top-frame 0
                              (run sched
                                   (make-state
                                    (list
                                     (cons 0
                                           (make-thread
                                            (push
                                             (make-frame
                                              0
                                              nil
                                              (push n nil)
                                              '((INVOKESTATIC "Demo" "fact" 1))
                                              'UNLOCKED
                                              "Demo")
                                             nil)
                                            'SCHEDULED
                                            nil)))
                                    *demo-heap*
                                    *demo-class-table*)))))))))

The following displays the M5 bytecode
corresponding to the fact method.

(lookup-method "fact" "Demo" *demo-class-table*)

Run the following to execute the bytecode on 5 and
get 120, and to execute the bytecode on 17 (negative
answer due to twos-complement representation of
lower 32 bits of result).

(demo-fact 5)
(demo-fact 17)

Compare with:

(! 17) ; factorial of 17 (previous name: fact)
(int-fix (! 17)) ; low 32 bits of 17 factorial

That is the negative number fact is returning:
``the low order 32 bits of the true factorial''.

Now prove correctness.  The summary shows rules
used in the proof.

(defthm fact-is-correct
  (implies (poised-to-invoke-fact th s n)
           (equal
            (run (fact-sched th n) s)
            (modify th s
             :pc (+ 3 (pc (top-frame th s)))
             :stack (push (int-fix (! n))
                          (pop (stack (top-frame th s)))))))
  :hints (("Goal"
           :induct (induction-hint th s n))))

The theorem above says that if you have an M5
state poised to execute the fact method on n in
thread th and if you run it a certain number to
steps on thread th, you just modify s by
incrementing the pc past the invoke instruction
(which is 3 bytes) and popping the n off the stack
and pushing the low order 32 bits of the true n!.