Creusot helps you prove your Rust code is correct
Recorded: May 28, 2026, 3:02 p.m.
| Original | Summarized |
GitHub - creusot-rs/creusot: Creusot helps you prove your Rust code is correct. · GitHub Skip to content Navigation Menu Toggle navigation
Sign in
Appearance settings PlatformAI CODE CREATIONGitHub CopilotWrite better code with AIGitHub SparkBuild and deploy intelligent appsGitHub ModelsManage and compare promptsMCP RegistryNewIntegrate external toolsDEVELOPER WORKFLOWSActionsAutomate any workflowCodespacesInstant dev environmentsIssuesPlan and track workCode ReviewManage code changesAPPLICATION SECURITYGitHub Advanced SecurityFind and fix vulnerabilitiesCode securitySecure your code as you buildSecret protectionStop leaks before they startEXPLOREWhy GitHubDocumentationBlogChangelogMarketplaceView all featuresSolutionsBY COMPANY SIZEEnterprisesSmall and medium teamsStartupsNonprofitsBY USE CASEApp ModernizationDevSecOpsDevOpsCI/CDView all use casesBY INDUSTRYHealthcareFinancial servicesManufacturingGovernmentView all industriesView all solutionsResourcesEXPLORE BY TOPICAISoftware DevelopmentDevOpsSecurityView all topicsEXPLORE BY TYPECustomer storiesEvents & webinarsEbooks & reportsBusiness insightsGitHub SkillsSUPPORT & SERVICESDocumentationCustomer supportCommunity forumTrust centerPartnersView all resourcesOpen SourceCOMMUNITYGitHub SponsorsFund open source developersPROGRAMSSecurity LabMaintainer CommunityAcceleratorGitHub StarsArchive ProgramREPOSITORIESTopicsTrendingCollectionsEnterpriseENTERPRISE SOLUTIONSEnterprise platformAI-powered developer platformAVAILABLE ADD-ONSGitHub Advanced SecurityEnterprise-grade security featuresCopilot for BusinessEnterprise-grade AI featuresPremium SupportEnterprise-grade 24/7 supportPricing Search or jump to... Search code, repositories, users, issues, pull requests...
Search Clear
Search syntax tips Provide feedback Include my email address so I can be contacted Cancel Submit feedback Saved searches
Name Query To see all available qualifiers, see our documentation. Cancel Create saved search Sign in Sign up
Appearance settings Resetting focus You signed in with another tab or window. Reload to refresh your session. Dismiss alert creusot-rs creusot Public
Notifications
Fork
Star Code Issues Pull requests Discussions Actions Projects Security and quality Insights
Additional navigation options
Code Issues Pull requests Discussions Actions Projects Security and quality Insights
masterBranchesTagsGo to fileCodeOpen more actions menuFolders and filesNameNameLast commit messageLast commit dateLatest commit History4,833 Commits4,833 Commits.github/workflows.github/workflows .vscode.vscode cargo-creusotcargo-creusot ci/htmlci/html creusot-argscreusot-args creusot-dev-configcreusot-dev-config creusot-installcreusot-install creusot-metadatacreusot-metadata creusot-rustccreusot-rustc creusot-setupcreusot-setup creusot-std-proccreusot-std-proc creusot-stdcreusot-std creusotcreusot examplesexamples exercisesexercises guideguide nixnix pearlite-synpearlite-syn prelude-generatorprelude-generator staticstatic teststests why3why3 why3testswhy3tests .gitattributes.gitattributes .gitignore.gitignore ARCHITECTURE.mdARCHITECTURE.md CHANGELOG.mdCHANGELOG.md CONTRIBUTING.mdCONTRIBUTING.md Cargo.lockCargo.lock Cargo.tomlCargo.toml INSTALLINSTALL LICENSELICENSE README.mdREADME.md comacoma creusot-deps.opamcreusot-deps.opam expandexpand flake.lockflake.lock flake.nixflake.nix fmtfmt ideide mirmir rust-toolchainrust-toolchain rustfmt.tomlrustfmt.toml tt testsuite_regeneratetestsuite_regenerate testsuite_upgrade_provertestsuite_upgrade_prover why3find.jsonwhy3find.json View all filesRepository files navigationREADMEContributingLGPL-2.1 license Le marteau-pilon, forges et aciéries de Saint-Chamond, Joseph-Fortuné LAYRAUD, 1889 Creusot
About Zeroing out a vector More examples are found in examples and tests/should_succeed. CreuSAT is a verified SAT solver written in Rust and verified with Creusot. It really pushes the tool to its limits and gives an idea of what 'use in anger' looks like. Installing Creusot as a user Install rustup, to get the suitable Rust toolchain Install Creusot: Check that the installation succeeded: See the Creusot guide: Installation Enter the cloned Creusot git repository used previously to install Creusot Update opam's package listing: Reinstall Creusot: Hacking on Creusot About Creusot helps you prove your Rust code is correct. creusot.rs Topics rust proof verification rust-lang formal-methods contracts formal-verification deductive-reasoning why3 Resources Readme LGPL-2.1 license Contributing Contributing Uh oh! There was an error while loading. Please reload this page. Activity Custom properties 1.6k 17 76 Report repository Releases Creusot v0.11.0 Latest Uh oh! There was an error while loading. Please reload this page. Contributors Uh oh! There was an error while loading. Please reload this page. Languages Rust JavaScript Nix Shell CSS HTML
Footer © 2026 GitHub, Inc. Footer navigation Terms Privacy Security Status Community Docs Contact Manage cookies Do not share my personal information You can’t perform that action at this time. |
Creusot is presented as a deductive verifier designed specifically for Rust code, functioning to establish the correctness and safety of the code by verifying that it is free from potential issues such as panics, overflows, and assertion failures. The core mechanism of Creusot involves translating the Rust code into Coma, which is an intermediate verification language provided by the Why3 Platform. This translation allows users to subsequently utilize the full capabilities of Why3 to semi-automatically discharge and verify the necessary conditions throughout the program's execution. The system relies on formal methods and deductive reasoning to achieve this verification, with technical details elaborated in the ARCHITECTURE.md file. Examples of the type of verification Creusot facilitates include mathematically verifying operations such as zeroing out a vector, performing binary search on vectors, sorting a vector, handling mutable iterations, and normalizing if-then-else expressions. This demonstrates the system's capacity to address complex logical and structural properties within code. Beyond general code verification, Creusot has been utilized in developing advanced projects, such as CreuSAT, which is a verified SAT solver written in Rust and proven correct using the Creusot framework. Creusot positions itself within the intersection of Rust programming, formal verification, and the Why3 ecosystem. For users interested in extending or modifying the system, the repository provides guidance on installation, which requires setting up the Rust toolchain and the OCaml package manager opam, cloning the repository, and executing the installation script. Further contributions to the codebase are managed through the CONTRIBUTING.md documentation, outlining the developer workflow. In essence, Creusot serves as a tool to apply rigorous mathematical proof techniques to ensure the correctness of Rust software. |