Frama-C doesn't actually prove memory safety and has a huge proof hole due to the nature of UB. It gives weaker guarantees than Rust in many cases. It's also far more of a pain to write. The Frama-C folks have been using the kernel as a testbed for years and contributing small patches back. The analysis just doesn't scale well enough to involve other people.

Spark doesn't have an active community willing to support its integration into the kernel and has actually been taking inspiration from Rust for access types. If you want to rustle up a community, go ahead I guess?