There's an older effort called Typed Assembly Language (TAL) by Greg Morrisett et al. It was a rather ambitious in some ways because it tried to model inter-procedural control flow, including exceptions. They eventually had a solution for array bounds checking, but I haven't seen anything for array initialization (that doesn't depend on a memory allocator that zeros everything or multi-instruction macros with semantics defined by fiat).