I don’t know the product, but you could certainly make a “secure iot “ device with C. Formal verification is again the search term you seek. System states. State machines being a good metaphor. Array bound checking doesn’t really matter if it’s a statically allocated array of a fixed known size. Arguably dynamic code vs static code is a bigger issue than language choice, and you see static code here in Hubris, and they explain why, so it’s not just about Rust but about the system design