Construct proof systems for common algorithmic task, like equivalence of regular expressions
You have a non-deterministic algorithm deciding the problem.
If you want to think of it as a proof system for $EQUIV$, then
the proof of $(u,v) \in EQUIVE$ is just the string 
representing the computation of your algorithm on $(u,v)$.
The proof checker just checks that 
the given string is in fact an accepting computation of your algorithm on $(u,v)$.

Use the alternative definition of proof system, it is often easier to think about: an algorithm that gets a formula and a string and checks if the string of a proof of the formula, rather than a function that checks if a given string of is proof and if so outputs the proven formula.