Abstract Context: Agile software development methods advocate the importance of producing working software without comprehensive documentation. While this approach seems to suit the evolutionary nature of realistic software development for many applications, even including safety-critical systems, it faces two major challenges. One is the lack of a comprehensible specification for code evolution and future maintenance, and the other is the potentially huge cost in code verification. Objective: To address this problem, we believe that supporting the efficient production of system specification by reversing the program constructed as the result of an agile development will be a useful solution. The reverse engineering of specifications from programs will not only help us produce the necessary specification for future program evolution, but more importantly can help us rigorously review the program to detect bugs for the enhancement of program quality. Method: In this paper, we put forward a novel method for rigorously reviewing code by reversing it into a comprehensible, formal specification. We elaborate on the principle of translating code into a specification and discuss how the translation process helps detect bugs in programs. We demonstrate how the proposed method works in practice with examples. We also present an experiment to evaluate the performance of the method by comparing it with existing checklist-based inspection. Conclusions: How to utilize reverse engineering of formal specifications from programs as a means to review the program for bug detection is an almost unexplored topic in software engineering. In this paper, we have described a specific method called RCRRE to reverse engineering of SOFL formal specifications from code and discussed how the reverse engineering process can be taken as an effective means to review the program for bug detection. The principle of converting code to a SOFL specification is reflected by a set of translation patterns and a two-step approach to construct a SOFL specification is established. To evaluate the performance, we have carried out an experiment on the effectiveness of our RCRRE method by comparing it with the CBI approach. The result of the experiment indicates that using our RCRRE method can effectively help the reviewer scrutinize the code and therefore find more bugs than the CBI when the reviewer is rather familiar with the SOFL specification language and skills. In the meanwhile, it also shows that the effectiveness of our RCRRE method may be affected in the situation where the reviewer lacks sufficient understanding and experience of SOFL, and using our RCRRE method may in general take a little longer time than the CBI.