Yes, for now we assume that there is exactly one answer for each external call to the system: https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#...

In practice, we should use a timeout in the implementation of all the external calls, but we did not and our model to not enforce it.