Idris 2 writes pretty quickly and you can prove the parts you want. It’s not blazingly fast but fast enough for many purposes and I definitely have far far less bugs and generally better code. Only for hobby projects so far but it is quite a brilliant.

It is verified implementation.