Asynchronous executions of robotic swarm algorithms are challenging to reason about because they allow robots to compute their next destination based on observations that may be outdated. To add formal guarantees in such a context where subtle mistakes lead to dramatic errors, we propose a formalization for the Rocq prover of asynchronous executions in the Look-Compute-Move model, as an extension to the Pactole formal library, and we illustrate how algorithms can be proved correct in this setting. Intuition makes it easy to overlook crucial details that formal methods would request when used, leading to published algorithms which can be, at best, seriously underspecified. This is particularly the case when problems seem easy, as with solving Gathering using Weber points. Attempts at formalization show that going blindly (or for that matter cautiously) towards the Weber point, a strategy often claimed to solve Gathering, is indeed incorrect under certain assumptions. We propose in this work an original and formally certified algorithm for Gathering in async. As this algorithm uses Weber points, we also provide a comprehensive formalization for Weber points and their properties. Interestingly, the use of our formalization for asynchronous executions does not come with an explosion of the proof size, which stays at a very reasonable level.