Inquiry: Feasibility of Using Verus for Verification in no_std and Zero-Dependency Environments

[HangShuYH]

Hello Verus team,

I am interested in using Verus for formal verification in a project that requires no_std environment and potentially minimal to no dependencies(eg: Rust-for-Linux). Could you please provide some guidance on the following:

no_std Compatibility

Is the Verus verifier itself compatible with no_std environments? If not, are there any plans to support it, or are there known workarounds?

Standard Library Dependencies

What are the specific parts of the Rust standard library that the Verus verifier currently relies on? Understanding these dependencies would help in assessing the effort required for no_std porting.

Minimal Dependency Configuration

Is there a minimal set of dependencies or a specific feature flag that can be used to reduce the dependency graph for use in constrained environments?

Future Roadmap

Does the project have any roadmap or ongoing efforts to make Verus more suitable for embedded systems or other no_std applications?

My target environment is no_std (and ideally no dependencies), commonly found in embedded systems, blockchain development, or other resource-constrained settings. Any insights, documentation, or pointers to relevant parts of the codebase would be greatly appreciated.

Thank you for your time and the great work on Verus!

[hiroki-chen]

vstd is no_std by simply adding no-default-features to the dependencies.