Is CBMC usable, directly, on any project? Or do you need to write your code in a certain way, using certain patterns, etc.? Or does the CBMC tooling need to b

Is CBMC usable, directly, on any project? Or do you need to write your code in a certain way, using certain patterns, etc.? Or does the CBMC tooling need to be taught various things about how memory management works in your project? Regardless, the fact that it's not used regularly/routinely with the Linux kernel (or any project that I'm aware of) suggests that it's either not suitable, doesn't catch enough issues to be worth the effort, or is just such a pain to deal with that no one has the patience to put up with it. Rust gives you much (sure, not all) of what CBMC provides, in the compiler. That is a huge win, IMO.