Formal Verification of a Rust-Based Buddy Physical Memory Allocator.

The physical memory allocator is a foundational component of an operating system, whose functional correctness is paramount for system reliability. Although Rust provides compile-time memory safety, it cannot guarantee the correctness of allocator-specific implementation logic. This paper presents the formal verification of UtManager, a Rust-based buddy physical memory allocator. Leveraging the Verus verification tool, we define state invariants and provide function specifications for the bitmap-based Rust implementation. We prove that operations such as allocation and free preserve these invariants and satisfy their postconditions, while ensuring bounds safety, overflow freedom, and termination. Notably, during verification, we uncovered and fixed a previously unknown control-flow defect in the original code. These results demonstrate that formal methods can enhance the reliability of Rust-based memory management components with zero runtime overhead.