This was an on-paper design I used to verify the data access patterns of a hardware bootloader that could write updates to chip config and flash from an encrypted payload using a hardware-protected AES PSK, all clocked by xmodem frames.
There are formal verification model systems that could be used here, but being able to reason aboult the totality of this system in one mindful was a key signal in the design process of this codebase.