We present the development and the validation of an algorithm for detecting the termination of diffusing computations. To the best of our knowledge, this is the first one which is based on the maximal paths generated by a diffusing computation. After an informal presentation of the algorithm, we proceed to its rigorous development within the framework of the Unity formalism and the assistance of the PVS proof system. The correctness of the algorithm is established through a refinement of an abstract model.