AlCoVe - Altered Coq Verification

AlCoVe (for Altered Coq Verification) is a project of formal verification in Coq of the rules of the game Altered.

Goals

This project aims to provide a Coq implementation of the Altered Comprehensive Rules (CompRules). This has several objectives :

• First, a complete implementation of the CompRules will show that the rules can indeed be formalized unambiguously
• It would allow to detect any loophole in the rules
• It would provide a tool to resolve rules questions with high confidence (but also kind of hard work if it needs an intricate proof)
• It will also provide tools to formally verify actual implementations of the game such as the Board Game Arena game or ExAltered to detect and prevent rule bugs.
• Whence the tool will be mature, it could also be used to create an app that automatically answer rule questions.

Coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem, or homotopy type theory), and teaching. (excerpt from Coq website)

Contribution

This project is initially developed by Orbion but anyone that is willing to help is invited to get involved. You can reach me directly or open issues or PRs.

Licence

This is an open source project, feel free to use this work in your own project. Please read the LICENCE file before doing so or fore more information.