During the task of acquiring formal specification, an important problem is verifing the correctness of acquired formal specification. In other words, given a problem requirement P, a variety of formal specifications will be acquired, but how to verify the correctness of them all? The different nature of the non- (semi-) formal of problem requirement and formal of specification makes it a challenging software problem and requirement for engineering. This paper proposes a formal derivation method to verify the relative correctness of different forms of Radl specifications corresponding same problem. It achieves this through a proof of the equivalency among different forms of Radl specifications and a certain formal specification S_i, which is straightforward to the problem requirement. S_i is converted into an execute program using PAR method and PAR platform, and is validated by test. In order to support the method, the study further put forth an extended logic system and aided certified algorithm. This paper uses Radl as formal specification language and elaborates the method using two typical examples in the domains of sort and search, combinational optimization. Practical effects manifest not only can effectively verify relatively correctness of Radl specification, but also has well extendibility. The method has potential theory significance and application value in research areas of formal specifications correctness verification, algorithms optimization and programs equivalency proof.