Does anyone have experience of using a tool like TLA+ to reproduce a minimal case of the kind of priority/mutex issue described on Mars? I’d be interested to know just how complicated (or not!) it would be for an interested hobbyist to use these tools to test out their diy microcontroller rtos, for example.
Not sure why they had to clickbait windows in the title. RTOSes are just as cool. I personally work With Nucleus at work but have dabbled with freertos for my pebble watch and vxworks just for fun.