  Previous works on formally studying mobile robotic swarms consider necessary
and sufficient system hypotheses enabling to solve theoretical benchmark
problems (geometric pattern formation, gathering, scattering, etc.). We argue
that formal methods can also help in the early stage of mobile robotic swarms
protocol design, to obtain protocols that are correct-by-design, even for
problems arising from real-world use cases, not previously studied
theoretically. Our position is supported by a concrete case study. Starting
from a real-world case scenario, we jointly design the formal problem
specification, a family of protocols that are able to solve the problem, and
their corresponding proof of correctness, all expressed with the same formal
framework. The concrete framework we use for our development is the PACTOLE
library based on the COQ proof assistant.
