The modelling of certain types of computational systems with classical logic includes limiting factors. In this context, the presentation of other logical systems, such as modal logic, and the construction of a library for the proof assistant Coq intents to help in the modelling and facilitate usage on the verification of systems' properties. The semantics of modal logic is represented by the semantics of possible worlds, where there is an accessibility relationship that connects the worlds of a model. Different restrictions imposed on the accessibility relation build modal logic systems that help representation of properties on a wide array of research areas. The libary development aims to held the formalization of properties in softwares and prove them on Coq.