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/