Instruction Set Architectures (ISA) are abstract models which specify the behavior of processors at the machine code level. They are now specified using custom programming languages such as Sail and ASL instead of being specified using prose. I will present a new, work-in-progress backend for the Sail compiler, which translates the ISA specifications into Lean code. I will then sketch how this fits in existing formalization efforts such as Lean-MLIR, a formalization of the MLIR intermediate representation and compiler infrastructure in Lean.