The Hack ALU allows for far more operations [text] for the C-instruction, than listed in the specification (ยง4.2.3). These could be utilized in a compiler targeting Hack for more efficient generated code.
Philip Zucker built a formally verified version of Nand to Tetris in Coq, nand2coq [notes].