Comment by fintler

Is there a TLA+ or Coq model available for this?