  The paper details the first successful attempt at using model-checking
techniques to verify the correctness of distributed algorithms for robots
evolving in a \emph{continuous} environment. The study focuses on the problem
of rendezvous of two robots with lights.
  There exist many different rendezvous algorithms that aim at finding the
minimal number of colors needed to solve rendezvous in various synchrony models
(e.g., FSYNC, SSYNC, ASYNC). While these rendezvous algorithms are typically
very simple, their analysis and proof of correctness tend to be extremely
complex, tedious, and error-prone as impossibility results are based on subtle
interactions between robots activation schedules.
  The paper presents a generic verification model written for the SPIN
model-checker. In particular, we explain the subtle design decisions that allow
to keep the search space finite and tractable, as well as prove several
important theorems that support them. As a sanity check, we use the model to
verify several known rendezvous algorithms in six different models of
synchrony. In each case, we find that the results obtained from the
model-checker are consistent with the results known in the literature. The
model-checker outputs a counter-example execution in every case that is known
to fail.
  In the course of developing and proving the validity of the model, we
identified several fundamental theorems, including the ability for a well
chosen algorithm and ASYNC scheduler to produce an emerging property of memory
in a system of oblivious mobile robots, and why it is not a problem for
luminous rendezvous algorithms.
