Coq Formal Verification

Open-source Coq projects categorized as Formal Verification

Top 5 Coq Formal Verification Projects

Formal Verification
  1. coq-of-rust

    Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦

    Project mention: Type-Constrained Code Generation with Language Models | news.ycombinator.com | 2025-05-13

    Yep, Rust famously goes beyond this by modelling memory ownership at compile time.

    In fact, the more behaviour we can model at compile time the better when it comes to LLMs - there's some cool ideas here like transpiling Rust into languages for formal verification. See https://github.com/formal-land/coq-of-rust as an example.

    Formal verification was one of those things that was previously so annoying to do that it rarely made it past academic use cases or extremely important libraries, but I think LLMs take the tedium out of it. Perhaps formal verification will have a "test driven development" type of moment in the sun thanks to this.

  2. InfluxDB

    InfluxDB – Built for High-Performance Time Series Workloads. InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.

    InfluxDB logo
  3. magmide

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

  4. proofs

    My personal repository of formally verified mathematics.

  5. ssprove

    A foundational framework for modular cryptographic proofs in Coq

    Project mention: There Is No Diffie-Hellman but Elliptic Curve Diffie-Hellman | news.ycombinator.com | 2025-05-28

    There is also SSProve which has similar goal to CryptHOL:

    https://dl.acm.org/doi/full/10.1145/3594735

    https://github.com/SSProve/ssprove

  6. aws-lc-verification

    This repository contains specifications, proof scripts, and other artifacts required to formally verify portions of AWS libcrypto. Formal verification is used to locate bugs and increase assurance of the correctness and security of the library.

    Project mention: How concurrecy works: A visual guide | news.ycombinator.com | 2024-12-20

    Agree. The remaining comments boil down to:

    1. "It's not visual, it's text". Yeah, but: how many "visual" representations have no text? And there _are_ visuals in there: the depictions of state space. They include text (hard to see how they'd be useful without) but aren't solely so.

    2. "Meh, verification is for well paid academics, it's not for the real world". First off, I doubt those "academics" are earning more than median sw devs, never mind those in the SV bubble. More importantly: there are well-publicised examples of formal verification being used for real-world code, see e.g. [1].

    It's certainly true that verification isn't widespread. It has various barriers, from use of formal maths theory and presentation to the compute load arising from combinatorial explosion of the state space. Even if you don't formally verify, understanding the state space size and non-deterministic path execution of concurrent code is fundamentally important. As Dijkstra said [2]:

    > our intellectual powers are rather geared to master static relations and that our powers to visualise processes evolving in time are relatively poorly developed. For that reason we should do (as wise programmers aware of our limitations) our utmost to shorten the conceptual gap between the static process and the dynamic program, to make the correspondence between the program (spread out in space) and the process (spread out in time) as trivial as possible.

    He was talking about sequential programming: specifically, motivating the use of structured programming. It's equally applicable to concurrent programming though.

    [1]: https://github.com/awslabs/aws-lc-verification

    [2]: https://homepages.cwi.nl/~storm/teaching/reader/Dijkstra68.p...

  7. SaaSHub

    SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

    SaaSHub logo
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).

Coq Formal Verification discussion

Log in or Post with

Coq Formal Verification related posts

  • How concurrecy works: A visual guide

    2 projects | news.ycombinator.com | 20 Dec 2024
  • Translation of the Rust's core and alloc crates to Coq for formal verification

    3 projects | news.ycombinator.com | 15 May 2024
  • Bertie – A minimal, high-assurance implementation of TLS 1.3 written in hacspec

    5 projects | news.ycombinator.com | 23 Mar 2024
  • A Taste of Coq and Correct Code by Construction

    3 projects | news.ycombinator.com | 3 Sep 2023
  • 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?

    2 projects | /r/rust | 4 Jul 2023
  • Announcing Magmide Month! (proof language for/using Rust)

    1 project | /r/rust | 28 Feb 2023
  • Formally Verifying Rust's Opaque Types

    2 projects | news.ycombinator.com | 1 Aug 2022
  • A note from our sponsor - InfluxDB
    www.influxdata.com | 23 Jun 2025
    InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now. Learn more →

Index

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

# Project Stars
1 coq-of-rust 923
2 magmide 821
3 proofs 301
4 ssprove 64
5 aws-lc-verification 50

Sponsored
InfluxDB – Built for High-Performance Time Series Workloads
InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.
www.influxdata.com

Did you know that Coq is
the 88th most popular programming language
based on number of references?