Hacker News Reader

https://sciendo.com/journal/FORMA gets close, I think (I don’t think it only publishes formally verified results. It likely also accepts more philosophical texts about formal verification). There’s also http://mizar.org/JFM/

I don’t think such journals can be the full solution, though.

Problem is that to entice mathematicians who don’t like formal verification to publish in it.

Homotopy type theory is just that: https://www.ias.edu/ideas/2014/voevodsky-origins

Homotopy type theory (HoTT) can mean several things: it's a new foundation of mathematics that was developed from the start with computer-formalization in mind. But you can also work on HoTT without ever touching a computer.

Conversely, there are many ways to do computer-formalization of mathematics, without every doing anything with HoTT.

What do you mean? Mathematics is all about formal verification, i.e. proofs.

I think they mean computer-verified proofs. As you note, the existing proofs are already formally verified, so this might not add much.