package coq-algorand

  1. Overview
  2. No Docs
A verified model of Algorand in Coq

Install

Dune Dependency

github.com Edit opam file Versions (3)

Authors

  1. M
    Musab A. Alturki
  2. J
    Jing Chen
  3. V
    Victor Luchangco
  4. B
    Brandon Moore
  5. K
    Karl Palmskog
  6. L
    Lucas Peña
  7. G
    Grigore Rosu

Maintainers

  1. P
    palmskog@gmail.com

Sources

release-1.2.tar.gz
sha512=f687c34da1800db35e7ef5a56e1eae918e016a7c3e5471995317c70de1084771563019e0adb132af1d92914e50b843cca197752bf56a63839e5ccf8feaf3cbd2

Description

The Algorand consensus protocol provides the foundation for a decentralized digital currency and transactions platform. This project provides a model of the protocol in Coq, expressed as a transition system over global states in a message-passing distributed system. Included is a formal proof of safety for the transition system.

Tags

category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keyword:distributed algorithms keyword:blockchain keyword:consensus keyword:algorand logpath:Algorand date:2020-07-24

Published: 24 Jul 2020

Dependencies (7)

  1. coq-record-update
  2. coq-interval >= "4.0.0"
  3. coq-mathcomp-analysis >= "0.3.1" & < "0.3.3~"
  4. coq-mathcomp-finmap >= "1.5"
  5. coq-mathcomp-algebra
  6. coq-mathcomp-ssreflect >= "1.11" & < "1.12~"
  7. coq >= "8.11" & < "8.12~"

Dev Dependencies

None

Used by

None

Conflicts

None