Maintenance 1.4 release supporting Coq 8.14

This is a maintenance release of the project, with the following features:

• Algorand model and safety proof from initial release
• support for Coq 8.14, 8.15, and 8.16 and Mathematical Components 1.14.0 and 1.15.0
• depend on mczify package that is part of the Coq Platform
• use fsfun update syntax from finmap 1.5.1
• fix deprecations

Maintenance 1.3 release supporting Coq 8.12

This is a maintenance release of the project, with the following features:

• Algorand model and safety proof from initial release
• support for Coq 8.12 and Mathematical Components 1.11.0
• remove dependency on Interval package
• change the type of a Value (block) from finType to the less restrictive choiceType
• improve code comments and compatibility with generated HTML documentation

Maintenance 1.2 release supporting Coq 8.11

This is a maintenance release that updates the project to support recent Coq and updated libraries, and includes:

• Algorand model and safety proof from initial release
• support for Coq 8.11 and Mathematical Components 1.11.0
• use of external libraries (mathcomp-analysis and coq-record-update) to simplify code

Maintenance 1.1 release supporting Coq 8.10

This is a maintenance release to coincide with the publication of a paper on the project in the 1st Workshop on Formal Methods for Blockchains (FMBC). It has the following features:

• Algorand model and safety proof from initial release
• support for Coq 8.10 and MathComp 1.9.0
• backwards-compatibility with Coq 8.9
• various improvements to the technical report

Model and Safety

This release defines the Algorand protocol and proves safety.