It's not that we have to choose one of those two options. Work is still being done on static-analysis tools for C.
To speak of Frama-C specifically, it isn't competing with new languages like Zig and Nim, it's competing with rival tools like [0], and with SPARK Ada. Formal reasoning about code is, for now, a niche reserved for critical-systems development. That kind of work tends to use tried-and-true languages with tried-and-true tooling: C, C++, Ada, and occasionally even Java.
> the languages we did design would be designed to make it easy to make tools that help us use them.
This is already a factor in language design. It's one of the reasons C-style preprocessors are now unfashionable.