It seems like step 2 is just validating that proofs are correct, and when it finds a problem, it doesn’t seem to do anything good about it.
The activity of step 2 results in proofs of statements like [A()==1 ⇒ U()==100] being long (in agent’s proof system, compared to length of proofs of the “natural” moral arguments like [A()==1 ⇒ U()==5]), something that wouldn’t be the case had step 2 been absent. So it does perform tangible work.
The activity of step 2 results in proofs of statements like [A()==1 ⇒ U()==100] being long (in agent’s proof system, compared to length of proofs of the “natural” moral arguments like [A()==1 ⇒ U()==5]), something that wouldn’t be the case had step 2 been absent. So it does perform tangible work.