  Voting procedures are designed and implemented by people, for people, and
with significant human involvement. Thus, one should take into account the
human factors in order to comprehensively analyze properties of an election and
detect threats. In particular, it is essential to assess how actions and
strategies of the involved agents (voters, municipal office employees, mail
clerks) can influence the outcome of other agents' actions as well as the
overall outcome of the election. In this paper, we present our first attempt to
capture those aspects in a formal multi-agent model of the Polish presidential
election 2020. The election marked the first time when postal vote was
universally available in Poland. Unfortunately, the voting scheme was prepared
under time pressure and political pressure, and without the involvement of
experts. This might have opened up possibilities for various kinds of ballot
fraud, in-house coercion, etc. We propose a preliminary scalable model of the
procedure in the form of a Multi-Agent Graph, and formalize selected integrity
and security properties by formulas of agent logics. Then, we transform the
models and formulas so that they can be input to the state-of-art model checker
Uppaal. The first series of experiments demonstrates that verification scales
rather badly due to the state-space explosion. However, we show that a recently
developed technique of user-friendly model reduction by variable abstraction
allows us to verify more complex scenarios.
