I'll read more later but just keep in mind nucleo is a series of form factors. There's even M33 on a -144 which is ARMv8-M

At a lower level in the formal verification stack than this, it's on the one hand awesome that ARM has published a machine readable architecture specification for the more recent A architectures in ASL... and on the other hand extremely frustrating that they haven't done the same for M.