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 |
| Unions | 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 |
| Supported (vstd equivalent) | |
| Crates and code organization | |
| Multi-crate projects | Partially supported |
| Verified crate + unverified crates | Partially supported |
| Modules | Supported |
| rustdoc | Supported |