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.
>>2
I'm learning Coq right now, what's wrong with it? It is fascinating but I have to admit it does not seem very practical for software.