The operating system serves as the foundational platform for software, and the security of its kernel is often of significant importance. Rust, a memory-safe language that has been gradually gaining popularity, incorporates safety mechanisms such as lifetimes, ownership, borrowing checks, and RAII. Building kernels using Rust has become a prominent area of research. However, systems constructed with Rust often contain some unsafe code segments, preventing the language from offering comprehensive guarantees of safety at the language level. Therefore, verifying these unsafe code segments is crucial for ensuring the correctness and reliability of Rust-based kernels. This paper proposes a method for combining the safe and unsafe code segments, called GhostFunc, to verify a microkernel built with Rust. The method applies different levels of abstraction to the two types of code segments and uses GhostFunc for the combination verification. Focusing on the task management and scheduling module, this paper formalizes unsafe code segments such as Arc<T> using λ_Rust and presents the formal implementation of GhostFunc. A verification example of this method is also provided. All verification work is based on theorem proving, and correctness is validated in Coq using the Iris separation logic framework.