You can get some information on contact tracing applications at

- Out of curiosity, I tried Lucy's suggestion to use (mod 2) instead of the definition of parity(·). It didn't work for me: all theorem provers / SMT solvers stop trying to prove

s ∈ ℕ ⊢ 1 - (s mod 2) = (s + 1) mod 2

which is precisely thee definition of parity I introduced as an axiom :-) This does not mean that theorem provers / SMT solvers are incredibly stupid. They have many compile-time configuration and invocation options and different theory modules that evolve and are improved continuously. It is possible that the matter is finding the right ones.

- A good, recent summary to learn about the status of contact tracing applications is

https://apnews.com/eb37b9ada939dfaff40925533c977b5c

(but if you do a Google search, many hits will appear)

The documents describing the DP3T proposal are at https://github.com/DP-3T/documents/blob/master/ , and the repositories under https://github.com/DP-3T have the source code.

Best,