I am not a Dafny expert but from what I have gathered it uses a deductive procedure underneath, so it's rather geared towards sequential code. To analyse concur

I am not a Dafny expert but from what I have gathered it uses a deductive procedure underneath, so it's rather geared towards sequential code. To analyse concurrent code, one needs to essentially build a sequential program that _also models the scheduler_ (see e.g., [1]). This procedure is unsurprisingly called sequentialization and (somewhat less unsurprisingly) is also a pretty good approach when applied to other techniques, such as bounded model checking [2]. [1] https://leino.science/papers/krml260.pdf https://leino.science/papers/krml260.pdf [2] https://research.cs.wisc.edu/wpis/papers/cav08.pdf https://research.cs.wisc.edu/wpis/papers/cav08.pdf