Ensuring the correctness of a given software component has become a crucial aspect in software engineering and model checking provides an almost fully automated way to achieve this goal.

In this paper we focus on the main issues for adding model checking functionality to the RAISE specification language and present the semantic foundations of our current approach for doing so. We also describe a way to use model checking to verify RAISE confidence conditions, ensuring the soundness and completeness (within certain finiteness constraints) of the results checked in this way. Finally, we present the most interesting details of the implementation of a tool that follows the described approach.