The operating system serves as the foundational platform for software, and the security of its kernel is often of paramount importance. Rust, a memory-safe programming language that has steadily gained popularity, incorporates safety mechanisms such as lifetimes, ownership, borrowing checks, and RAII. Using Rust to build kernels has emerged as a prominent area of research. However, systems built with Rust often include some unsafe code segments, which prevent the language from offering comprehensive safety guarantees at the language level. As a result, verifying these unsafe code segments is essential to ensuring the correctness and reliability of Rust-based kernels. This study proposes a method for combining the safe and unsafe code segments, called GhostFunc, to verify a microkernel constructed with Rust. Different levels of abstraction are applied to the two types of code segments, and GhostFunc is used for combined verification. Focusing on the task management and scheduling module, this study formalizes unsafe code segments such as Arc<T> using λ_Rust and presents the formal implementation of GhostFunc. An example verification of this method is also provided. All verification efforts are based on theorem proving, and correctness is validated in Coq using the Iris separation logic framework.