Verified Software Toolchain
-
Updated
Aug 6, 2024 - Coq
Verified Software Toolchain
A framework for formally verifying distributed systems implementations in Coq
Correctness proofs of Ethereum token contracts
Coq formalizations of functional languages.
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs!
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
An implementation of a simple asynchronous message-passing lock server, verified in Coq using the Verdi framework
Formally verified Coq serialization library with support for extraction to OCaml
A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators
Intermediate Memory Model (IMM) and compilation correctness proofs for it
Proofs of correctness for "Partial Aborts for Software Transactional Memory" formalized in Coq
Various sorting algorithms formalised using the "sauto" component of CoqHammer 1.3.
Formalisation of the linear lambda calculus in Coq
A small coq library for verifying OCaml native integer computations
Add a description, image, and links to the proof topic page so that developers can more easily learn about it.
To associate your repository with the proof topic, visit your repo's landing page and select "manage topics."