VST
Formal verification toolkit
A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant
Verified Software Toolchain
444 stars
23 watching
93 forks
Language: Coq
last commit: 2 months ago ccompcertcoqcoq-librarycoq-vstformal-methodsformal-specificationformal-verificationproofproof-assistantverification
Related projects:
| Repository | Description | Stars |
|---|---|---|
 formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 292 |
| formal-land/coq-of-rust | Tool that verifies Rust code by translating it into Coq's proof system to ensure no bugs or vulnerabilities exist | 437 |
 vlopezj/coq-course | A self-reading Coq course for PhD students covering fundamental topics in functional programming and formal verification. | 38 |
 coq/vscoq | An extension for Visual Studio Code and VSCodium to support Coq Proof Assistant | 349 |
 coq-community/coq-program-verification-template | A template project for verifying the correctness of C programs in Coq | 29 |
 smtcoq/smtcoq | An OCaml-based plugin for Coq that verifies and extends proof witnesses from external SAT/SMT solvers | 157 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 153 |
 princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 388 |
 huynhtrankhanh/coqcp | Verifying competitive programming solutions to catch errors and improve rigor through formal mathematical proof | 22 |
 cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 351 |
 mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |
 certicoq/veriffi | Enables verified interaction between Coq programs and C libraries | 39 |
| coq-community/coq-ext-lib | A collection of reusable Coq definitions and theorems for building software development tools | 129 |