Title: Toward a foundational typed assembly language
A paper from 2002 but a very interesting read; it formally defines a type system for a complete assembly language (TAL). The paper gives typing rules for the instructions and for memory allocation; its advantages are verification and reasoning (for things like heap object reachability) with machine-checked proofs.
An implementation (in OCaml) of TAL for x86 is TALx86; includes a type-checker and an assembler.
Original Twitter link: https://twitter.com/_argp/statuses/524588812731969536