A surprise, from the README:
"HiRTOS is formally specified using the Z notation. The Z specification can be found here [link]."
I used Z years ago. I haven't seen any new work in Z for many years -- but the linked specification is dated in 2024.
Also, "The HiRTOS thread scheduler is formally specified in TLA+/Pluscal. The TLA+/Pluscal specification can be found here [link] It was model-checked using the TLC model checker. The sucessful TLC run [link] took more than 7 hours"
