It's not so much fundamental advances as much as a maturing of tooling and educational resources. The result is a lot of compelling proof-of-concept implementations:

https://sel4.systems/

http://compcert.inria.fr/

https://cakeml.org/