Is it possible for it to work with async code

[ple1n]

I'm writing a small tool for configuring linux system. which contains some async code. I'm in the middle of refactoring my code and libs to be generic over sync/async-ness as a workaround (with proc macros). I'm not even sure how much formal reasoning can help in this case. It's just an attempt. Verifying a terminally imperative program sounds cool too.

Verus, Prusti, Mirai all don't work with async. I think they work with multi-threading ? Is it theoretically hard, or just lacking implementation ?