W moim referacie opowiem o niektórych zagrożeniach, jakie dla procedur wyborczych stwarza (bądź zwiększa) użycie nowoczesnych technologii informacyjnych. Przedstawię również pewne pomysły, jak odporność na te zagrożenia może być specyfikowana i weryfikowana w logice temporalnej czasu alternującego z elementem epistemicznym. Tematyka referatu związana jest z rozpoczętym niedawno projektem VoteVerif w ramach polsko-luksemburskiego programu PolLux.