The following form is designed to provide information for your tool that should be included in the effort to verify the Rust standard library. Please note that the tool will need to be supported if it is to be included.

Tool Name

Please enter your tool name here.

Description

Please enter a description for your tool and any information you deem relevant.

Tool Information

Does the tool perform Rust verification?
Does the tool deal with unsafe Rust code?
Does the tool run independently in CI?
Is the tool open source?
Is the tool under development?
Will you or your team be able to provide support for the tool?

Comparison to Other Approved Tools

Describe how this tool compares to the other approved tools. For example, are there certain properties that this tool can prove that the other tools cannot? The comparison does not need to be exhaustive; the purpose of this section is for the committee to understand the salient differences, and how this tool would fit into the larger effort.

Licenses

Please list the license(s) that are used by your tool, and if to your knowledge they conflict with the Rust standard library license(s).

Steps to Use the Tool

[First Step]
[Second Step]
[and so on...]

Artifacts & Audit Mechanisms

If there are noteworthy examples of using the tool to perform verification, please include them in this section. Links, papers, etc. Also include mechanisms for the committee to audit the implementation and correctness of this tool (e.g., regression tests).

Versioning

Please describe how you version the tool.

CI

If your tool is approved, you will be responsible merging a workflow into this repository that runs your tool against the standard library. For an example, see the Kani workflow (.github/workflows/kani.yml). Describe, at a high level, how your workflow will operate. (E.g., how will you package the tool to run in CI, how will you identify which proofs to run?).

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!