DataProVe is a tool that allows a user to specify a high-level data protection (or privacy) policy and a system architecture, then verify the conformance between the specified architecture and the high-level policy.  

The main goal of the tool is to help a system designer at the higher level (compared to other tools that mainly focus on the protocol/implementation level.), such as with the policy and architecture design. This step can be important to spot high-level design flaws early, before going ahead with the lower level system specification. 

DataProVe may be useful for education purposes as well, especially, where the subject is about personal data protection or privacy.  

The verification engine of DataProVe is based on logic ("guided" resolution based proofs), combining both the so-called backward and forward search strategies.

DataProVe comes with a graphical user interface, and the current version is written in Python.  

The GitHub page of the tool can be found here: LINK

The paper about the theoretical background of the tool can be read here: PoPETs 2022 paper.  (Long Pre-print version: Report)

In the following, we present two intro videos of the tool (1st video - high level intro, 2nd video - verification of real life contact tracing approaches). 

The video below shows the verification of a version of real-life contact tracing approaches used in some European countries (DP3T https://github.com/DP-3T/documents  and PEPP-PT https://github.com/pepp-pt/pepp-pt-documentation)