i've been meaning to look into Typed Assembly Language! https://www.cs.cornell.edu/talc/overview.html

The goal of the TAL project is to extend the paradigm of type-directed compilation to its limit. We compile high-level languages that include features such as higher-order polymorphic functions, datatypes, modules, objects, and subtyping into a series of typed intermediate languages and finally into a Typed Assembly Language (TAL). Unlike any other compiler, we not only use typed intermediate languages but also typed target languages.

[...]

The type soundness of our assembly code implies many important security properties such as memory safety. As a result, our assembly code is a form of proof-carrying code.