Comment by mimd

No, it can track pointer bounds and validity across functions. It also targets identifying cases of UB via eva. Both rust and frama-C rely on assertions to low level memory functions. Rust has the same gaping UB hole in unsafe that can cross into safe.

If we are talking about more than memory, such as what greg is talking about in encoding operational properties then no, rust is far behind both frama-C, Spark, and tons of others. They can prove functional correctness. Or do you think miri, kani, cruesot, and the rest of the FM tools for Rust are superfluous?

My mocking was that that the kernel devs have had options for years and have ignored them out of dislike (ada and spark) or lack of effort (frama-C). That other options provide better solutions to some of their intrests. And that this is more a project exercise in getting new kernel blood than technical merits.