Formally Verified and Publicly Verifiable E-counting For Complex Voting Schemes

I will first explain single transferable vote counting and the parlous state of computer-counting code implemented by various Election Commissions from around Australia. I will then explain how we used Coq to specify a "vanilla" version of single transferable voting as a proof-calculus and used it to extract a computer program which not only counts votes according to this specification but also produces a certificate during the count. The specification of the certificate is derived from the counting rules. We have proved, in Coq, that if the certificate is correct with respect to its specification, then the result it encapsulates must be correct with respect to the relevant specification of single transferable voting. The certificate is designed so that an average third-year computer science student could write a computer program to check the correctness of the certificate.