For asynchronous code, it's important to be able to spawn tasks. Since tokio::spawn or something similar will be difficult to support, we should provide our own version that is optimized for Kani. Part of #1393