Supported Rust Features

Quick reference for supported Rust features. Note that this list does not include all Verus features, and Verus has many spec/proof features without any standard Rust equivalent—this list only concerns Rust features. See the guide for more information about Verus’ distinction between executable Rust code, specification code, and proof code.

Note that Verus is in active development. If a feature is unsupported, it might be genuinely hard, or it might just be low priority. See the github issues or discussions for information on planned features.

Last Updated: 2024-06-26

Items
Functions, methods, associated functions Supported
Associated constants Not supported
Structs Supported
Enums Supported
Const functions Partially supported
Async functions Not supported
Macros Supported
Type aliases Supported
Const items Partially supported
Static items Partially supported
Struct/enum definitions
Type parameters Supported
Where clauses Supported
Lifetime parameters Supported
Const generics Partially Supported
Custom discriminants Not supported
public / private fields Partially supported
Expressions and Statements
Variables, assignment, mut variables Supported
If, else Supported
patterns, match, if-let, match guards Supported
Block expressions Supported
Items Not supported
loop, while Supported
for Partially supported
? Supported
Async blocks Not supported
await Not supported
Unsafe blocks Supported
& Supported
&mut, place expressions Partially supported
==, != Supported, for certain types
Type cast (as) Partially supported
Compound assigments (+=, etc.) Supported
Array expressions Partially supported (no fill expressions with `const` arguments)
Range expressions Supported
Index expressions Partially supported
Tuple expressions Supported
Struct/enum constructors Supported
Field access Supported
Function and method calls Supported
Closures Supported
Labels, break, continue Supported
Return statements Supported
Integer arithmetic
Arithmetic for unsigned Supported
Arithmetic for signed (+, -, *) Supported
Arithmetic for signed (/, %) Not supported
Bitwise operations (&, |, !, >>, <<) Supported
Arch-dependent types (usize, isize) Supported
Types and standard library functionality
Integer types Supported
bool Supported
Strings Supported
Vec Supported
Option / Result Supported
Floating point Not supported
Slices Supported
Arrays Supported
Pointers Partially supported
References (&) Supported
Mutable references (&mut) Partially supported
Never type Not supported
Function pointer types Not supported
Closure types Supported
Trait objects (dyn) Not supported
impl types Partially supported
Cell, RefCell Not supported (see vstd alternatives)
Iterators Not supported
HashMap Not supported
Smart pointers (Box, Rc, Arc) Supported
Pin Not supported
Hardware intrinsics Not supported
Printing, I/O Not supported
Panic-unwinding Not supported
Traits
User-defined traits Supported
Default implementations Supported
Trait bounds on trait declarations Supported
Traits with type arguments Partially supported
Associated types Partially supported
Generic associated types Partially supported (only lifetimes are supported)
Higher-ranked trait bounds Supported
Clone Supported
Marker traits (Copy, Send, Sync) Supported
Standard traits (Hash, Debug) Not supported
User-defined destructors (Drop) Not supported
Sized (size_of, align_of) Supported
Deref, DerefMut Not supported
Multi-threading
Mutex, RwLock (from standard library) Not supported
Verified lock implementations Supported
Atomics Supported (vstd equivalent)
spawn and join Supported
Interior mutability Supported
Unsafe
Raw pointers Supported (only pointers from global allocator)
Transmute Not supported
Unions Supported
UnsafeCell Supported (vstd equivalent)
Crates and code organization
Multi-crate projects Partially supported
Verified crate + unverified crates Partially supported
Modules Supported
rustdoc Supported