There is VLisp, which is a verified implementation of Scheme ( https://sci-hub.ru/10.1007/BF01128406 ). Rees' W7 kernel is also interesting ( http://mumble.net/~jar/pubs/secureos/secureos.html ). It's not formally proven, but definitely engineered for reliability. It lives on in Scheme48 ( https://www.s48.org/ ) which used to be my favourite Scheme impl, but seems moribund now.
But if you're interested in proving theorems, the simple ones of type theory seem relevant, so perhaps you should use a statically typed language?. I think CakeML is a better route to explore issues like this nowadays ( https://github.com/CakeML/cakeml ). On the other hand I'm slightly disillusioned with anything more complex than a SystemF-like type system with sums, products as in *ML or Haskell, etc. So if it looks like I have to prove general theorems in HOL, Coq or dependent types, I take a step back. This led me from CakeML to just SML.