Have you heard of https://cakeml.org/? It's a self-hosting formally verified compiler.

Thank you, I've heard of it. It is indeed very close to what I want to have. CakeML project also has a language Pancake, which has interesting properties.

Here's the list of projects which I'm aware of: https://github.com/m1el/riscv-fv-bootstrap/tree/master/docs/...