On: Muen Kernel: Trustworthy by Design – Correct By Construction

[aetherspawn]

Signed up just to comment on this. I've been wanting to do something similar for a while now (although, an exokernel).

You should update your source to use the new 2014 tools. The verifications become part of the syntax.

[zobzu → aetherspawn]

yeah verifications part of the code syntax seems like a decent concept for such cases