Your projects are multilanguage. 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. Learn more →
Top 17 Coq coq Projects

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  20220915
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/.

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 🚀.


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

verdiraft
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
Raft has been manually verified which was the hurdle here that makes the result interesting:


kami
A Platform for HighLevel Parametric Hardware Specification and its Modular Verification (by mitplv)
Project mention: There's an ongoing effort to rewrite Principia Mathematica using Coq  reddit.com/r/math  20211203There are ongoing research projects about that, you may want to have a look at Kôika (https://github.com/mitplv/koika), Kami (https://github.com/mitplv/kami), Lutsig (https://github.com/CakeML/hardware) and silveroak (https://github.com/projectoak/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 indemand technologies, state of the remote work... all you need to know your worth on the market by tech recruitment platform talent.io



Project mention: There's an ongoing effort to rewrite Principia Mathematica using Coq  reddit.com/r/math  20211203
There are ongoing research projects about that, you may want to have a look at Kôika (https://github.com/mitplv/koika), Kami (https://github.com/mitplv/kami), Lutsig (https://github.com/CakeML/hardware) and silveroak (https://github.com/projectoak/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.

coqlibraryundecidability
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  20220821I want to run guix shell to create an environment with the dependencies required to build coqlibraryundecidability.

Project mention: There's an ongoing effort to rewrite Principia Mathematica using Coq  reddit.com/r/math  20211203
There are ongoing research projects about that, you may want to have a look at Kôika (https://github.com/mitplv/koika), Kami (https://github.com/mitplv/kami), Lutsig (https://github.com/CakeML/hardware) and silveroak (https://github.com/projectoak/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.

PS: Obligatory plug for hstocoq.

Project mention: Rupicola: Relational Compilation for PerformanceCritical Applications  reddit.com/r/Compilers  20220617

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 coqsimpleio 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/adventofcoq2018/blob/master/sol/day01_1.v

Project mention: Aneris: Program logic for developing and verifying distributed systems  news.ycombinator.com  20220918


SonarQube
Static code analysis for 29 languages.. Your projects are multilanguage. 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.
Coq coq related posts
 What is the need of formally verified compilers? Where are they used? Do verified compiler support all features that unverified compiler do?
 Development Environment with guix shell for Coq Package
 Formally Verifying Rust's Opaque Types
 New Coq tutorial
 Ask HN: Can the same individual accomplish more with programming than proofs?
 It took Russell and that other guy 360 pages to prove that 1+1=2. That's how rigorous math is.
 Which is the most abstract and bizzare book of mathematics you have ever came across?

A note from our sponsor  SonarQube
www.sonarqube.org  26 Sep 2022
Index
What are some of the best opensource coq projects in Coq? This list will help you:
Project  Stars  

1  CompCert  1,455 
2  proofs  228 
3  CoqEquations  186 
4  principia  180 
5  verdiraft  163 
6  fourcolor  122 
7  kami  116 
8  corn  104 
9  toychain  98 
10  koika  94 
11  coqlibraryundecidability  81 
12  vericert  63 
13  hstocoq  61 
14  rupicola  42 
15  coqsimpleio  24 
16  aneris  21 
17  doublygeneric  4 
Are you hiring? Post a new remote job listing for free.