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 verifi

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.