Libraries

The Verus standard library, vstd, comes with a variety of utilities and datatypes for proofs, as well as runtime functionality with specifications. Most Verus programs will start with use vstd::prelude::*;, which pulls in a default set of definitions that we find generally useful. This chapter will introduce a few of them, but you can find more complete descriptions in the vstd documentation.