Threading and async are an issue with the current CProver core. But, much of that can be simulated by writing helper functions that get shadowed during the model checking.
It's simply not possible to make a bounded model checker work on arbitrary code, so instead, the code should be factored to work within the constraints of the model checker. The result is safer code, even if the style is different.
I never said threading. I use a single-threaded runtime. But the lack of any async support even though it’s basically syntactic sugar at that point makes it a non-starter. There’s some amount of “make your code testable” that’s valid, but completely rewrite how your application is written and thus you can’t use the frameworks you need to is a bit much. At some point the testing framework has to also meet you where you are.
kani certainly could be extended to have better async / await support. But, I think this is a larger engineering problem. The value of code that has been verified using an existing model checking tool is greater than the value of code using a particular framework and hoping that Some Day there will exist a tool that will work with that framework.
I'd wrap libraries that were problematic to build function contracts around before I punted on model checking. Hell, I'd fork and refactor these APIs to work with lightweight fibers before I gave up on model checking. The utility of something like async / await is small potatoes compared to the utility of having code that has even light formal verification in place.
It's simply not possible to make a bounded model checker work on arbitrary code, so instead, the code should be factored to work within the constraints of the model checker. The result is safer code, even if the style is different.