coq-of-python
Coq verifier
Formal verification of Python code using Coq
Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python.
30 stars
1 watching
0 forks
Language: Coq
last commit: 2 months ago Related projects:
| Repository | Description | Stars |
|---|---|---|
| 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 | 421 |
| formal-land/coq-of-ocaml | Transforms OCaml code into formal, verifiable Coq code to prove complex properties | 255 |
 sec-bit/tokenlibs-with-proofs | Verifies the correctness of Ethereum token contracts using formal methods and proof assistants. | 98 |
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 442 |
 mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |
 thery/coqprime | A proof assistant library for prime number certification using elliptic curves and Pocklington certificates | 37 |
 bedrocksystems/brick | Formalization of C++ logic for verifying concurrent programming | 69 |
| ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
| formal-land/coq-bonsai | Generates a random Coq program with a graphical tree-like structure | 24 |
 mmcco/verified-parser-example | A formally verified parser implementation using Coq and OCaml | 20 |
 coq-community/gaia | A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics | 28 |
| coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
| coq-community/bits | A formalization of bitset operations in Coq with extraction to OCaml native integers. | 22 |