With the development of cloud computing, it is becoming increasingly important to enhance security through isolated execution environments such as sandboxes and TEEs. However, isolation execution environments rely on trusted computing bases (TCBs) such as the OS kernel and hypervisor, which themselves become more difficult to guarantee security as system software becomes increasingly complex. To address this problem, our approach focuses on security-critical components, in particular reference monitors. As the reference monitor operates at the interface between the isolation execution environment and the TCB system software and handles input from attackers directly, it is a cost-effective approach to intensify security in that area through formal verification. However, formal verification of reference monitors requires modelling their behaviour, which is not easy because the wide variety of inputs to reference monitors and the security policies they implement make it difficult to cover all patterns. As a first step in this approach, this study targets reference monitors at the system call level, aiming in particular to overcome the challenge of time-of-day attacks (TOCTTOU) that occur during the monitoring of system calls. Specifically, it aims to ensure that reference monitors can correctly enforce a given security policy for system calls issued at any given time and in any given order by introducing a two-stage thorough verification using automatic verification code generation and parallel verification.