busycoq
BusyBeaverDecider
A project providing verified implementations of Busy Beaver deciders using Coq proof and verification.
Busy Beaver deciders backed by Coq proof
39 stars
6 watching
6 forks
Language: Coq
last commit: 7 months ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 351 |
 engineeringsoftware/mcoq | Analyze and test Coq proof assistant projects by generating modified versions of the code to identify flaws in specifications. | 30 |
 dboulytchev/minikanren-coq | A certified semantics for relational programming language specification, providing verified implementations of syntax and semantics for miniKanren languages | 26 |
| cpitclaudel/alectryon | A tool for processing Coq and Lean 4 code embedded in text documents | 237 |
 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/alea | A library for reasoning about randomized algorithms in Coq | 25 |
| 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 |
 benmorris/netarchtest | Enforces architectural rules in .Net codebases to promote consistent design and maintainability | 1,424 |
| coq-community/bits | A formalization of bitset operations in Coq with extraction to OCaml native integers. | 22 |
| coq-community/autosubst | Automates formalizing syntactic theories with variable binders in Coq | 52 |
 whonore/coqtail | Enables interactive proof development in Vim similar to other proof assistants. | 274 |
 absint/compcert | A formally verified compiler for a subset of C that generates code for multiple architectures. | 1,901 |
 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 |
 mmcco/verified-parser-example | A formally verified parser implementation using Coq and OCaml | 20 |