jscert
JavaScript verifier
A Coq-based verification of the ECMAScript 5 standard for a JavaScript interpreter
A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter
196 stars
24 watching
12 forks
Language: Coq
last commit: over 1 year ago
Linked from 2 awesome lists
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 jscoq/jscoq | An online development environment for the proof assistant Coq, allowing users to run and interact with it in their browser. | 518 |
 ymherklotz/vericert | A tool for formally verifying high-level synthesis of digital circuits | 88 |
 absint/compcert | A formally verified compiler for a subset of C that generates code for multiple architectures. | 1,901 |
 coq-community/coq-program-verification-template | A template project for verifying the correctness of C programs in Coq | 29 |
 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 |
 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 |
 certicoq/veriffi | Enables verified interaction between Coq programs and C libraries | 39 |
 certigraph/certigraph | A verification toolset for graph-manipulating programs written in Coq. | 17 |
 josefgit/concert | A framework for verifying smart contracts in Coq, a proof assistant language. | 0 |
| formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
| coq-community/autosubst | Automates formalizing syntactic theories with variable binders in Coq | 52 |
 engineeringsoftware/mcoq | Analyze and test Coq proof assistant projects by generating modified versions of the code to identify flaws in specifications. | 30 |
 siimplex/concert | A framework for verifying smart contracts in Coq | 1 |