Proof software for Primitive Recursive Arithmetic
The ACL2 theorem prover seems quite close to what you want, though it is hard to know exactly what the strength of the system is.

From the logical description here it looks like the base is a quantifier-free equational logic with induction principles, which include principles allowing the definition of PR functions.

This gives exactly PRA, but in addition, the standard library defines induction up to $\varepsilon_0$, which brings the strength up to full Peano Arithmetic.

You might therefore want to work in ACL2 with a restricted version of the standard induction principle (I don't know how hard that is).