<p>With their unmatched expansion in recent years, online social networks (OSNs) have become not only one of the most effective modes for viral publicity but also the foremost source of news amongst people nowadays. However, these promising features come with the possibility of rumor propagation that can lead to unwanted situations. Due to the enormous number of users on these platforms, there is a substantial challenge in containing the viral spread of rumors on a large scale proficiently. Existing research, conducted in various domains, exclusively depends on simulations to determine whether the proposed model is error-prone. In this paper, a Colored Petri net (CPN)-based formal verification was carried out to specify, analyze, and validate crowdsource-based rumor verification. The formal model is analyzed through state space generation to illustrate how predefined behavioral properties can be verified. Moreover, the formal verification of the rumor verification model is evaluated based on generated simulations to track the origin of errors during debugging. For validation of the proposed CPN model, a state space report is generated, which contains beneficial information regarding behavioral properties of the model, i.e., boundedness, liveness, and fairness properties. Moreover, experimental evaluation is performed, and outcomes show that a formally verified CPN-based rumor detection model achieves superior accuracy compared to recent state-of-the-art approaches, offering a reliable and interpretable approach for detecting misinformation in online social networks. To the best of our knowledge, CPN formalization has never been accomplished for crowdsource-based rumor verification, so this research can provide interesting insights into the behavior of the crowd as well as the specifications and requirements of such a system.</p>