coq-of-ocaml
Code transformer
Transforms OCaml code into formal, verifiable Coq code to prove complex properties
Formal verification for OCaml
255 stars
8 watching
20 forks
Language: OCaml
last commit: 4 months ago
Linked from 2 awesome lists
compilercoqocaml
Related projects:
| Repository | Description | Stars |
|---|---|---|
| formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
| 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 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
 smorimoto/coq-to-ocaml-to-js | Generates safe and fast JavaScript code from mathematical proofs using Coq, OCaml, BuckleScript, Rollup, Terser, and Closure Compiler | 25 |
 coq/vscoq | A Visual Studio Code extension for Coq proof assistant support | 343 |
 smtcoq/smtcoq | An OCaml-based plugin for Coq that verifies and extends proof witnesses from external SAT/SMT solvers | 156 |
 mmcco/verified-parser-example | A formally verified parser implementation using Coq and OCaml | 20 |
| ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 ocaml-community/sedlex | A tool for generating Unicode-friendly lexers in OCaml | 240 |
 ocaml-ppx/ppx_deriving | A library simplifying type-driven code generation in OCaml | 466 |
 coq-community/bits | A formalization of bitset operations in Coq with extraction to OCaml native integers. | 22 |
| coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
| formal-land/coq-bonsai | Generates a random Coq program with a graphical tree-like structure | 24 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 442 |