A Lean tactic for Canonical, a search procedure for terms in dependent type theory.

This program introduces formal verification to card-based cryptography by providing a technique which automatically finds new protocols using as few as possible operations and searches for lowest bounds on card-minimal protocols.

Towards automatic voting rule argumentation by using computer-aided verification such as software bounded model checking.