Machine-checked Foundations for Verified Vote Counting

该项目将为在优先选举中计票的许多共同系统制定议会法案的正式逻辑说明的一般方法。该项目将提供相应的计算机程序，根据这些系统进行计票，并将提供正式的、独立的、可核查的证据，证明这些程序符合其规格。这种经过正式验证的计算机程序为计算机计票提供了法律上可靠的基础。该方法还将使选举专员能够改进对议会相关法案的自然语言描述，这些法案往往与目前的做法不合时宜，令人遗憾。

The project will deliver a general methodology for developing formal logical specifications of the Acts of Parliament for many common systems for counting votes in preferential elections. The project will deliver corresponding computer programs to count votes according to these systems and will deliver formal independently checkable proofs that the programs meet their specification. Such formally verified computer programs provide a legally sound basis for counting votes by computer. The methodology will also allow electoral commissioners to improve the natural language descriptions of the relevant Acts of Parliament which are often woefully out of date with current practice.