This is a great achievement in making formal methods accessible in pragmatic terms - something that actually works and can be used by normal humans.

Would be nice to have an actual microcontroller example.

> The standard library is fully stack based and heap allocation is strongly discouraged

:/ - I can see why this is done, as it's hard, so banning it to make the problem tractable works. But it's also quite inconvenient. On the other hand, "MISRA C:2004, 20.4 - Dynamic heap memory allocation shall not be used."