The goal of my research is to improve the quality of software. I use for that the field of formal methods, in order to define precisely the behavior of programs. This allows to reason rigorously about these behaviors, to detect unwanted, potentially dangerous states for example. In this talk, I will present my ongoing contribution to Mopsa, a multilanguage static analysis platform relying on abstract interpretation. It is able to detect all potential runtime errors within C programs, Python programs and programs mixing these two languages. I will present our first participation to the Software-Verification Competition. The goal of this competition is to be able to automatically (dis)prove specific properties on given programs. This event gathered 50 different software verifiers this year, and Mopsa earned a bronze medal in the “Software Systems” category.