From cfdc94f2f6dbb8cd9d11354daf9e8e6ba2a40b12 Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Tue, 10 Feb 2026 16:53:27 -0500 Subject: [PATCH 1/2] Add guidelines for what goes into vstd and how to publish Verus crates on crates.io. --- CONTRIBUTING.md | 59 +++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 57 insertions(+), 2 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 22fa33493f..d61b370c76 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -6,7 +6,7 @@ contributions. Please report issues or start discussions here on GitHub. We use GitHub discussions for feature requests and more open-ended conversations about upcoming features, and we reserve GitHub issues for actionable issues (bugs) with existing features. Don't worry though: if we think an issue should be a discussion (or -viceversa) we can always move it later. +vice versa) we can always move it later. ## Reporting an issue @@ -143,6 +143,23 @@ this for VS Code. ## Contributing to the standard library (`vstd`) +### What to contribute + +Verus aims to curate `vstd` along similar lines to how Rust curates `std`. +Ideally, `vstd` should contain a set of minimal shared abstractions (and proofs +about them) to enable the larger Verus community to develop their own +abstractions and proof techniques. A particularly important use case for +`vstd` is supporting the abstractions needed to provide specs for Rust's `std`, +so that people developing with Verus can use standard Rust constructs without +relying on external dependencies. + +If your contribution doesn't fall into this minimal subset, it may +be better off as an independent package published on [crates.io](https://crates.io), +which the community can then integrate via `cargo verus`. See the +[Best Practices](best-practices-for-publishing-verusverified-code-on-cratesio) below. + +### Tips for testing and verifying your contribution + If you're contributing to the standard library, you should also test the standalone build of that library with ``` @@ -169,11 +186,49 @@ cd source/vstd ../target-verus/release/verus --crate-type=lib --is-vstd vstd.rs --cfg 'feature="std"' --cfg 'feature="alloc"' ``` -### Common Conventions +### Common conventions Inside `vstd`: - We add a `lemma_` prefix to the name of a lemma (i.e., a `proof fn`) to make its purpose explicit. - We try to make lemmas associated functions when possible, e.g., `my_map.lemma_remove_keys_len(keys)`, not `lemma_remove_keys_len(my_map, keys)`. +## Best practices for publishing Verus-verified code on crates.io + +[Publishing](https://doc.rust-lang.org/cargo/reference/publishing.html) +your Verus-verified crate on [crates.io](https://crates.io) is a great +way to enable more people to build on your hard work. If you do so, we encourage +you to follow these best practices. +1. If your crate is primarily for specification and proof purposes (i.e., a normal Rust developer + is unlikely to benefit from it), then please make this clear in your preamble (i.e., in the README.md + file that appears on the crates.io landing page. For example, you might say: + "This crate contains formal specifications and proofs about Widgets, + primarily for use with [Verus](https://github.com/verus-lang/verus), a tool + for verifying the correctness of Rust code." +2. If your crate contains verified executable Rust code that could be used by both unverified + and verified projects, you might instead say something like: "This crate + implements Widgets with the following fun features: [Feature list]. The + code has been formally verified using [Verus](https://github.com/verus-lang/verus), + which means [list of properties you proved, with suitable caveats for what + properties have not been proven]." It's important to convey the limitations + of your proof (e.g., what you may have assumed about other libraries), so that + consumers of your crate are not disappointed when something breaks. Err on the + side of under-promising and over-delivering. +3. If your crate contains verified executable Rust code that uses any of Verus's + wrappers around unsafe primitives (e.g., raw pointers), then we encourage you + to run the [safe API checker](https://verus-lang.github.io/verus/guide/calling-verified-from-unverified.html), + which can detect places where your external interface relies on Verus-checked + preconditions to ensure safety. It's important to remember that unverified + consumers are not subject to these checks, so providing such an + interface may lead to undefined behavior. The [guide](https://verus-lang.github.io/verus/guide/calling-verified-from-unverified.html) + offers some tips on how to improve such an interface. +4. We encourage you to apply [verusdoc](https://verus-lang.github.io/verus/guide/verusdoc.html) + to your crate. Like `rustdoc`, `verusdoc` will automatically generate nice + HTML documentation, and it will also include Verus-related specifications. + Ideally, you should host this documentation online and provide a link to it + in the preamble of your package on crates.io. In addition, adding a CI job + to your repository to automatically update your documentation site will + help keep it in sync as your package evolves. + + ## Other tips You can use `--vstd-no-verify` to skip verification of the `vstd` library. This is pretty useful if you're building or running tests a lot. Note that it will still _build_ `vstd`—it just skips the SMT step. For example: From 9d50922af9823eef1bf5b88645a64f3bd51e708f Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Fri, 13 Feb 2026 14:36:07 -0500 Subject: [PATCH 2/2] Clarify unsafe caveat based on Travis's suggestion. --- CONTRIBUTING.md | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index d61b370c76..20d1ac26b3 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -212,13 +212,19 @@ you to follow these best practices. of your proof (e.g., what you may have assumed about other libraries), so that consumers of your crate are not disappointed when something breaks. Err on the side of under-promising and over-delivering. -3. If your crate contains verified executable Rust code that uses any of Verus's - wrappers around unsafe primitives (e.g., raw pointers), then we encourage you - to run the [safe API checker](https://verus-lang.github.io/verus/guide/calling-verified-from-unverified.html), - which can detect places where your external interface relies on Verus-checked - preconditions to ensure safety. It's important to remember that unverified - consumers are not subject to these checks, so providing such an - interface may lead to undefined behavior. The [guide](https://verus-lang.github.io/verus/guide/calling-verified-from-unverified.html) +3. If your crate contains verified executable Rust code that uses any of + Verus's unsafe primitives ([raw + pointers](https://verus-lang.github.io/verus/verusdoc/vstd/raw_ptr/index.html), + [PPtr](https://verus-lang.github.io/verus/verusdoc/vstd/simple_pptr/struct.PPtr.html), + or + [PCell](https://verus-lang.github.io/verus/verusdoc/vstd/cell/pcell/struct.PCell.html)) + or uses explicit `unsafe` blocks, then we encourage you to run the [safe API + checker](https://verus-lang.github.io/verus/guide/calling-verified-from-unverified.html), + which can detect places where your external interface relies on + Verus-checked preconditions to ensure safety. It's important to remember + that unverified consumers are not subject to these checks, so providing such + an interface may lead to undefined behavior. The + [guide](https://verus-lang.github.io/verus/guide/calling-verified-from-unverified.html) offers some tips on how to improve such an interface. 4. We encourage you to apply [verusdoc](https://verus-lang.github.io/verus/guide/verusdoc.html) to your crate. Like `rustdoc`, `verusdoc` will automatically generate nice