coq-of-rust
Code verifier
Tool that verifies Rust code by translating it into Coq's proof system to ensure no bugs or vulnerabilities exist
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦
437 stars
9 watching
17 forks
Language: Coq
last commit: almost 2 years agocoqformal-verificationproofrust
Related projects:
| Repository | Description | Stars |
|---|---|---|
| formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
| formal-land/coq-of-ocaml | Transforms OCaml code into formal, verifiable Coq code to prove complex properties | 255 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 444 |
 mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |
 engineeringsoftware/mcoq | Analyze and test Coq proof assistant projects by generating modified versions of the code to identify flaws in specifications. | 30 |
| formal-land/coq-bonsai | Generates a random Coq program with a graphical tree-like structure | 24 |
 jscert/jscert | A Coq-based verification of the ECMAScript 5 standard for a JavaScript interpreter | 196 |
 xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
 verifytests/verify.moq | Adds Verify support for Moq types to verify mock behavior and assertions | 14 |
 rafaelcgs10/w-in-coq | A Coq formalization of Damas-Milner type system and its algorithm W for verifying the correctness of type inference tools. | 25 |
 sec-bit/tokenlibs-with-proofs | Verifies the correctness of Ethereum token contracts using formal methods and proof assistants. | 97 |
 coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 153 |