Yeah, I've done something similar twice for embedded systems. First one was modelling a BLE protocol between a mobile device and a piece of hardware to confirm

Yeah, I've done something similar twice for embedded systems. First one was modelling a BLE protocol between a mobile device and a piece of hardware to confirm that the protocol the vendor provided would definitively lose messages in specific circumstances. The second was to model the LoRaWAN protocol as a state machine and prove that the SM model I'd put together couldn't deadlock; the C implementation of it modelled the TLA+ model very closely. I was honestly pretty shocked that after getting the first version of the implementation done there was exactly one bug in it and it was a typo (used the wrong variable somewhere) and not a logic error. Other than that the implementation basically worked perfectly first try and just kept running indefinitely.