https://github.com/verus-lang/verus Skip to content Navigation Menu Toggle navigation Sign in * Product + Actions Automate any workflow + Packages Host and manage packages + Security Find and fix vulnerabilities + Codespaces Instant dev environments + Copilot Write better code with AI + Code review Manage code changes + Issues Plan and track work + Discussions Collaborate outside of code Explore + All features + Documentation + GitHub Skills + Blog * Solutions For + Enterprise + Teams + Startups + Education By Solution + CI/CD & Automation + DevOps + DevSecOps Resources + Learning Pathways + White papers, Ebooks, Webinars + Customer Stories + Partners * Open Source + GitHub Sponsors Fund open source developers + The ReadME Project GitHub community articles Repositories + Topics + Trending + Collections * Pricing Search or jump to... Search code, repositories, users, issues, pull requests... Search [ ] Clear Search syntax tips Provide feedback We read every piece of feedback, and take your input very seriously. [ ] [ ] Include my email address so I can be contacted Cancel Submit feedback Saved searches Use saved searches to filter your results more quickly Name [ ] Query [ ] To see all available qualifiers, see our documentation. Cancel Create saved search Sign in Sign up You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert {{ message }} verus-lang / verus Public * Notifications * Fork 37 * Star 417 * Verified Rust for low-level systems code License MIT license 417 stars 37 forks Branches Tags Activity Star Notifications * Code * Issues 64 * Pull requests 17 * Discussions * Actions * Wiki * Security * Insights Additional navigation options * Code * Issues * Pull requests * Discussions * Actions * Wiki * Security * Insights verus-lang/verus This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository. main BranchesTags Go to file Code Folders and files Last commit Last Name Name message commit date Latest commit History 2,556 Commits .github/workflows .github/workflows .vscode .vscode dependencies dependencies source source tools tools .git-blame-ignore-revs .git-blame-ignore-revs .gitignore .gitignore CONTRIBUTING.md CONTRIBUTING.md INSTALL.md INSTALL.md LICENSE LICENSE README.md README.md rust-toolchain.toml rust-toolchain.toml View all files Repository files navigation * README * License Quick Start Library Documentation project chat Verus is a tool for verifying the correctness of code written in Rust. Developers write specifications of what their code should do, and Verus statically checks that the executable Rust code will always satisfy the specifications for all possible executions of the code. Rather than adding run-time checks, Verus instead relies on powerful solvers to prove the code is correct. Verus currently supports a subset of Rust (which we are working to expand), and in some cases, it allows developers to go beyond the standard Rust type system and statically check the correctness of code that, for example, manipulates raw pointers. VS Code Demo Status Verus is under active development. Features may be broken and/or missing, and the documentation is still incomplete. If you want to try Verus, please be prepared to ask for help in the Zulip. Try Verus To try Verus in your browser, please visit the Verus Playground. For more involved development, please follow our installation instructions. Then you can dive into the documentation below, starting with the Tutorial and reference. Documentation Our (work-in-progress) documentation resources include: * Tutorial and reference * API documentation for Verus's standard library * Guide for verifying concurrent code * Project Goals * Contributing to Verus * License Getting in touch, reporting issues, and starting discussions Please report issues or start discussions here on GitHub, or join us on Zulip for more realtime discussions and if you need help. Thank you for using and contributing to Verus! 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 vice versa) we can always move it later. We welcome contributions! If you'd like to contribute code, have a look at the tips in Contributing to Verus. --------------------------------------------------------------------- Zulip Zulip sponsors free hosting for Verus. Zulip is an open-source modern team chat app designed to keep both live and asynchronous conversations organized. About Verified Rust for low-level systems code Resources Readme License MIT license Activity Custom properties Stars 417 stars Watchers 20 watching Forks 37 forks Report repository Releases No releases published Packages 0 No packages published Contributors 30 * @utaal * @tjhance * @Chris-Hawblitzel * @parno * @chanheec * @utaal-b * @jaybosamiya * @yizhou7 * @jaylorch * @mmcloughlin * @isubasinghe * @tchajed * @achreto * @jonhnet + 16 contributors Languages * Rust 99.7% * Shell 0.2% * HTML 0.1% * Dockerfile 0.0% * PowerShell 0.0% * Nix 0.0% Footer (c) 2024 GitHub, Inc. Footer navigation * Terms * Privacy * Security * Status * Docs * Contact * Manage cookies * Do not share my personal information You can't perform that action at this time.