Coq coq

Open-source Coq projects categorized as coq Edit details

Top 17 Coq coq Projects

  • CompCert

    The CompCert formally-verified C compiler

    Project mention: What is the need of formally verified compilers? Where are they used? Do verified compiler support all features that unverified compiler do? | reddit.com/r/compsci | 2022-09-15

    Languages are often not verified in full, because doing so might be a tremendous task, and you often don't need to verify a whole language. Often just a subset of the features will allow you to do what you need to. One example of a partially verified C language: https://compcert.org/.

  • proofs

    My personal repository of formally verified mathematics.

    Project mention: Formally Verifying Rust's Opaque Types | news.ycombinator.com | 2022-08-01

    It's always a pleasant surprise to see people using Coq and other formal verification technology. We need more rigor in programming! If this article gave you a thirst for interactive theorem proving and you want to learn it from the ground up, I've recently written a Coq tutorial [1] which covers topics like programming with dependent types, writing proofs as data, and extracting verified code. That repository also contains a handy tactic called `eMagic` [1] (a variant of another useful tactic called `magic` which solve goals with existentials) which can automatically prove the theorem from the article.

    [1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...

    [2] https://github.com/stepchowfun/proofs/blob/56438c9752c414560...

  • Scout APM

    Truly a developer’s best friend. Scout APM is great for developers who want to find and fix performance issues in their applications. With Scout, we'll take care of the bugs so you can focus on building great things 🚀.

  • Coq-Equations

    A function definition package for Coq

  • principia

    The Principia Rewrite (by LogicalAtomist)

    Project mention: Principia Mathematica in modern notation. | reddit.com/r/math | 2022-07-21

    You can check it out here: https://www.principiarewrite.com/

  • verdi-raft

    An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

    Project mention: Paxos automatically determined safe and secure | news.ycombinator.com | 2021-10-27

    Raft has been manually verified which was the hurdle here that makes the result interesting:

    https://github.com/uwplse/verdi-raft

  • fourcolor

    Formal proof of the Four Color Theorem [[email protected]]

  • kami

    A Platform for High-Level Parametric Hardware Specification and its Modular Verification (by mit-plv)

    Project mention: There's an ongoing effort to rewrite Principia Mathematica using Coq | reddit.com/r/math | 2021-12-03

    There are ongoing research projects about that, you may want to have a look at Kôika (https://github.com/mit-plv/koika), Kami (https://github.com/mit-plv/kami), Lutsig (https://github.com/CakeML/hardware) and silveroak (https://github.com/project-oak/silveroak). Closer to HLS there is also Vericert (https://github.com/ymherklotz/vericert). There may be other research project I am unaware of, feel free to add them in a reply, I am interested in it.

  • talent.io

    Download talent.io’s Tech Salary Report. Median salaries, most in-demand technologies, state of the remote work... all you need to know your worth on the market by tech recruitment platform talent.io

  • corn

    Coq Repository at Nijmegen [[email protected],@VincentSe]

  • toychain

    A minimalistic blockchain consensus implemented and verified in Coq

  • koika

    A core language for rule-based hardware design 🦑

    Project mention: There's an ongoing effort to rewrite Principia Mathematica using Coq | reddit.com/r/math | 2021-12-03

    There are ongoing research projects about that, you may want to have a look at Kôika (https://github.com/mit-plv/koika), Kami (https://github.com/mit-plv/kami), Lutsig (https://github.com/CakeML/hardware) and silveroak (https://github.com/project-oak/silveroak). Closer to HLS there is also Vericert (https://github.com/ymherklotz/vericert). There may be other research project I am unaware of, feel free to add them in a reply, I am interested in it.

  • coq-library-undecidability

    A library of mechanised undecidability proofs in the Coq proof assistant.

    Project mention: Development Environment with guix shell for Coq Package | reddit.com/r/GUIX | 2022-08-21

    I want to run guix shell to create an environment with the dependencies required to build coq-library-undecidability.

  • vericert

    A formally verified high-level synthesis tool based on CompCert and written in Coq.

    Project mention: There's an ongoing effort to rewrite Principia Mathematica using Coq | reddit.com/r/math | 2021-12-03

    There are ongoing research projects about that, you may want to have a look at Kôika (https://github.com/mit-plv/koika), Kami (https://github.com/mit-plv/kami), Lutsig (https://github.com/CakeML/hardware) and silveroak (https://github.com/project-oak/silveroak). Closer to HLS there is also Vericert (https://github.com/ymherklotz/vericert). There may be other research project I am unaware of, feel free to add them in a reply, I am interested in it.

  • hs-to-coq

    Convert Haskell source code to Coq source code.

    Project mention: agda2hs, verify your haskell code in agda? | reddit.com/r/haskell | 2022-01-04

    PS: Obligatory plug for hs-to-coq.

  • rupicola

    Gallina to Bedrock2 compilation toolkit

    Project mention: Rupicola: Relational Compilation for Performance-Critical Applications | reddit.com/r/Compilers | 2022-06-17
  • coq-simple-io

    IO for Gallina

    Project mention: Advent of Code Day 1 | reddit.com/r/Coq | 2022-02-04

    It's possible to do all that work still in Coq, so that the extracted code can directly be compiled into an executable. One way is to use the coq-simple-io library, which basically wraps the OCaml standard library (including functions for reading and writing files/stdin/stdout) as Coq axioms. For example, I did extraction that way in a previous iteration of AoC: https://github.com/Lysxia/advent-of-coq-2018/blob/master/sol/day01_1.v

  • aneris

    Program logic for developing and verifying distributed systems

    Project mention: Aneris: Program logic for developing and verifying distributed systems | news.ycombinator.com | 2022-09-18
  • doubly-generic

    Arity-generic datatype-generic, or doubly-generic, programming in Coq.

  • SonarQube

    Static code analysis for 29 languages.. Your projects are multi-language. So is SonarQube analysis. Find Bugs, Vulnerabilities, Security Hotspots, and Code Smells so you can release quality code every time. Get started analyzing your projects today for free.

NOTE: The open source projects on this list are ordered by number of github stars. The number of mentions indicates repo mentiontions in the last 12 Months or since we started tracking (Dec 2020). The latest post mention was on 2022-09-18.

Coq coq related posts

Index

What are some of the best open-source coq projects in Coq? This list will help you:

Project Stars
1 CompCert 1,455
2 proofs 228
3 Coq-Equations 186
4 principia 180
5 verdi-raft 163
6 fourcolor 122
7 kami 116
8 corn 104
9 toychain 98
10 koika 94
11 coq-library-undecidability 81
12 vericert 63
13 hs-to-coq 61
14 rupicola 42
15 coq-simple-io 24
16 aneris 21
17 doubly-generic 4
Find remote jobs at our new job board 99remotejobs.com. There are 5 new remote jobs listed recently.
Are you hiring? Post a new remote job listing for free.
Static code analysis for 29 languages.
Your projects are multi-language. So is SonarQube analysis. Find Bugs, Vulnerabilities, Security Hotspots, and Code Smells so you can release quality code every time. Get started analyzing your projects today for free.
www.sonarqube.org