This isn't new, it is actually part of how Dafny came to be, another formal verification programming language.
"Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System"
https://www.microsoft.com/en-us/research/publication/safe-to...
However so far hardly anyone in mainstram cared about verified assembly, maybe now with LLMs.
"Programming Language Design and Implementation in the Era of Machine Learning"
https://www.youtube.com/watch?v=Fc3cW0nqAQ0