Top 3 Coq Formal Verification Projects

magmide

3 778 0.0 Coq

A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

Project mention: Languages on the rise like Rust and Go are being quite vocal against inheritance and many engineers seem to agree. Is this the end of inheritance? What do you think? | /r/rust | 2023-07-04

https://github.com/magmide/magmide when
proofs

2 272 0.0 Coq

My personal repository of formally verified mathematics.

Project mention: A Taste of Coq and Correct Code by Construction | news.ycombinator.com | 2023-09-03

If you're already familiar with a functional programming language like Haskell or OCaml, you have the prerequisite knowledge to work through my Coq tutorial here: https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...
My goal with this tutorial was to introduce the core aspects of the language (dependent types, tactics, etc.) in a "straight to the point" kind of way for readers who are already motivated to learn it. If you've heard about proof assistants like Coq or Lean and you're fascinated by what they can do, and you just want the TL;DR of how they work, then this tutorial is written for you.
Any feedback is appreciated!
Mergify

blog.mergify.com
sponsored

Tired of breaking your main and manually rebasing outdated pull requests?. Managing outdated pull requests is time-consuming. Mergify's Merge Queue automates your pull request management & merging. It's fully integrated to GitHub & coordinated with any CI. Start focusing on code. Try Mergify for free.
hacspec

0 222 0.0 Coq

A specification language for cryptography primitives.

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 2023-09-03.