FWIW -- A later, vaguely related project was Jitawa[1]. Its Lisp dialect was not as fancy as VLISPs, but its verification was much more thorough (machine checked proofs down to the X86 code for the runtime.)

Today, ongoing, CakeML[2] extends these techniques to an ML language and is just generally super awesome.

[1] https://www.cl.cam.ac.uk/~mom22/jitawa/ [2] https://cakeml.org/

People may also be interested in BitC[0] in regards to verified lisp languages.

[0]: http://yamm.finance/wiki/BitC.html (the best summary I could find)

Cool work.

I wonder if contemporary proof assistants have enough primitives to implement this.