An emergent trend has recently received significant attention: networks of passively and/or actively mobile sensors (that is, swarms of robots). These robots are able to execute collectively various complex tasks; one application being for example to optimise the coverage of interest zones under natural or human disaster, and help in search and rescue tasks. A characteristic feature is the extreme dynamism of their structure, content, load, and even execution environment. Possibly the subjects to Byzantine failures, obtaining certified guarantees on their behaviour is a crucial issue, as they belong to an area of computer science well-known for being remarkably harsh on informal reasoning, possibly leading to disastrous errors when arguments are not perfectly clear. Project SAPPORO aims to propose a formal provable framework (mechanised in the (awarded) Coq proof assistant) to assess the correctness of localised distributed protocols at the core of dynamic mobile sensor networks.