The vostd project provides a formally-verified version of OSTD, the (unofficial) standard library for OS development in safe Rust. OSTD encapsulates low-level hardware interactions—which requires using unsafe Rust—into a small yet powerful set of high-level, safe abstractions. These abstractions enable the creation of complex, general-purpose OSes like Asterinas entirely in safe Rust.
By design, OSTD guarantees soundness: no undefined behavior is possible, regardless of how its API is used in safe Rust. The goal of the vostd project is to bolster confidence in this soundness through formal verification, leveraging the Verus verification tool.
This work is ongoing. Our current focus is on verifying OSTD’s memory management subsystem, a core component that is directly related to kernel memory safety. As we continue, we aim to extend formal verification to additional parts of OSTD to further ensure its reliability and correctness.
Implementation code from the OSTD mainline, together with its accompanying proofs, resides in the aster_common and ostd directories, while specifications are located under specs.
This repository currently contains verification code for ostd/src/mm and ostd/src/boot/memory_region.rs. It is independent of the concurrency proofs presented in our SOSP paper — “CortenMM: Efficient Memory Management with Strong Correctness Guarantees.” For the SOSP artifact, please refer to the func-correct branch for verification code, and to this repo for the complete artifact.
A merge of these efforts is planned, but has not yet begun.
If you have not installed Rust yet, follow the official instructions.
vostd relies on our custom build tool, which serves as a more powerful alternative to cargo-verus. Please run:
git submodule update --init --recursive
You can build Verus with the following command:
cargo dv bootstrap
Verus should be automatically cloned and built in the tools directory. If download fails, please clone the repo manually into tools/verus , then run cargo dv bootstrap again.
To verify the entire project, simply run:
cargo dv verify --targets ostd
The ostd crate relies on two verified libraries: vstd_extra and aster_common. To compile and verify these libraries independently, run:
cargo dv compile --targets vstd_extra
cargo dv compile --targets aster_common
dv automatically skips recompilation and reverification for libraries that have not changed since the last build. To remove all build artifacts and force a fresh build, run:
cargo dv clean --targets vstd_extra
cargo dv clean --targets aster_common
You can also run cargo dv clean to clean all artifacts at once.
For VSCode users, the verus-analyzer extension is available in the Marketplace.
For Emacs users, please refer to the verus-mode.
We welcome your contributions!
- We add an
axiom_prefix to the name of eachaxiom fnand alemma_prefix to eachproof fn. - We prefer associated functions to isolated lemmas.
- During your development process, please frequently run
cargo dv bootstrap --upgradeto stay up-to-date with the latest supported version of Verus. - Format checking is currently disabled due to instability in
verusfmt, but we still recommend formatting your code withverusfmtbefore submission. - If you are contributing to Verus, we recommend submitting pull requests to the official repo rather than our fork, since we aim to minimize differences between them.