Having learned a number of Lisp systems in the past, I wouldn't necessarily recommend ANSI Common Lisp as a first choice for a Lisp unless your needs are very particular, because it is an enormous design-by-committee language having a draft standard of about 1360 pages:

  https://lisp.com.br/archive/ansi_cl_standard_draft_nice.pdf

This means that in addition to the time spent doing the programming that solves your technical problem, you also have to devote considerable time to language lawyering, investigating if the interpretation of a Lisp expression your Common Lisp produces is or is not standard conforming, using only the frequently ambiguous English of that enormous standard as your guide.

The Java JVM was carefully designed to give identical results on all hosts for the Java platform unless you go out of your way to get nondeterminism or platform specific behavior (make the value of the number N depend on thread scheduling, or use JNI that assumes a platform byte order, etc.). C/C++/Rust allow undefined behavior if you shift a 64-bit int more than 64 bits, but Java on the JVM for example masks the lower 6 bits of a 64-bit shift ('& 0x3f') so that you get the same result on all CPUs rather than a CPU-dependent result:

  https://docs.oracle.com/javase/specs/jls/se8/html/jls-15.html#jls-15.19

The nice thing about this is that the JVM makes a "try it and see" approach more viable: if your program has a bug at least it has the same bug everywhere. You won't suddenly get a crash 10 years in the future when your customers upgrade to a new CPU, because your Java bytecodes on their new CPU will faithfully maintain bug-for-bug compatibility.

Clojure is a Lisp that runs on the JVM. I haven't personally used Clojure, but having done quite a bit of Common Lisp, Emacs Lisp, Scheme, etc., it looks to be very well designed and very well loved by its users, and using it could spare you from having to language lawyer the ANSI Common Lisp standard, as it seems to be more "try it and see" friendly.

I've been learning a lot about formal verification for C programs, how to truly make code that is bug free, and to do this you need to first make certain decisions about how you are going to formalize the language standard. E.g. will you assume that CHAR_BIT==8 or will you allow CHAR_BIT>=8 because the official ANSI/ISO C standard allows this even though all modern computers have CHAR_BIT==8? Then for any program you input to your verifier you must judge whether all its behavior is well-defined or if there is undefined behavior (arithmetic overflow, etc.).

There are quite good formal verification tools for Java, also, like JBMC and Krakatoa, and smaller Lisp languages are traditionally among the least tedious to formally verify (very simple semantics, unlike Common Lisp), but the time investment to learn these tools is enormous.