HiRTOS: A high-integrity multi-core RTOS kernel written in SPARK Ada

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"