Hi Nirnai Rai,
as far as I know, nobody is currently working on formal verification of any sorts. The current projects to improve security are:
- Improving Rust support in RIOT
- Rust support is actually pretty mature at the moment, but not every board supports Rust as of now and not every feature implemented in C in RIOT is wrapped as Rust API yet
- A number of core developers are aiming to implement more and more features in Rust. Once Rust support is mature enough that this would become practical, I expect some formal proposal to actually do this
- A number of modern MCU have features like MPUs that do a allow a meaningful distinction between userspace threads and kernel threads
- with that, it would be possible to limit a thread to only access its own memory and only access hardware via syscalls, very similar to what e.g. Linux does
- multiple options to run code in a VM
It would be interesting to see work on formal verification 