Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications!
-
Updated
Apr 2, 2025 - Coq
#
proof
Here are 33 public repositories matching this topic...
A framework for formally verifying distributed systems implementations in Coq
-
Updated
May 17, 2024 - Coq
Verified Software Toolchain
c coq proof verification proof-assistant formal-methods compcert formal-verification coq-library formal-specification coq-vst
-
Updated
Apr 2, 2025 - Coq
Coq formalizations of functional languages.
-
Updated
Jul 2, 2020 - Coq
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
-
Updated
Jul 26, 2024 - Coq
Correctness proofs of Ethereum token contracts
-
Updated
Jun 5, 2019 - Coq
Intermediate Memory Model (IMM) and compilation correctness proofs for it
-
Updated
Feb 5, 2025 - Coq
Formally verified Coq serialization library with support for extraction to OCaml
-
Updated
Oct 22, 2023 - Coq
A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators
-
Updated
Jan 7, 2023 - Coq
An implementation of a simple asynchronous message-passing lock server, verified in Coq using the Verdi framework
-
Updated
Oct 23, 2017 - Coq
Formalisation of the linear lambda calculus in Coq
-
Updated
Dec 2, 2018 - Coq
He Reiter, Ho Reiter, He Reiter, Immer weiter!
-
Updated
Mar 1, 2024 - Coq
Formal proof that closure conversion with flat environments is safe for space.
-
Updated
Jun 1, 2019 - Coq
Proofs of correctness for "Partial Aborts for Software Transactional Memory" formalized in Coq
-
Updated
May 26, 2016 - Coq
-
Updated
Jul 31, 2018 - Coq
Improve this page
Add a description, image, and links to the proof topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the proof topic, visit your repo's landing page and select "manage topics."