This is a talk about how we can generate single transferable votes counting code from a logical specification automatically using advanced computer aided verification methods.
It is based upon a PhD dissertation but I think I made it non-technical.