verified-parser-example
Formal Parser
A formally verified parser implementation using Coq and OCaml
A minimal example of a formally verified parser using ocamllex and Menhir's Coq backend.
20 stars
2 watching
1 forks
Language: Coq
last commit: over 10 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 verifytests/verify.moq | Adds Verify support for Moq types to verify mock behavior and assertions | 14 |
 coq/vscoq | An extension for Visual Studio Code and VSCodium to support Coq Proof Assistant | 349 |
 formal-land/coq-of-ocaml | Transforms OCaml code into formal, verifiable Coq code to prove complex properties | 255 |
| formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
 coq-community/comp-dec-modal | Machine-checked proofs of soundness, completeness, and decidability for modal logics in Coq. | 8 |
 smtcoq/smtcoq | An OCaml-based plugin for Coq that verifies and extends proof witnesses from external SAT/SMT solvers | 157 |
| coq-community/parseque | A Coq library that provides a total parser combinator library with support for building parsers and grammars in the language of Coq. | 42 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 444 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 292 |
| coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
 ocaml-community/iso8601.ml | A parser and printer for date-times in ISO8601 format. | 29 |
 certicoq/veriffi | Enables verified interaction between Coq programs and C libraries | 39 |
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 pa-ba/calc-comp | Formalizations of compiler design and virtual machine calculations in Coq | 30 |
 uwplse/cheerios | A formally verified serialization library for Coq | 23 |