Programs use rules to dictate or constrain specific decisions or actions. These rules have typically been tested, revised, and updated continuously; therefore, they represent a substantial and valuable business or intellectual asset. These rules often are not reused because the legacy program code is the only valid source for these rules, and extraction of the rules from the legacy code is thought to be too difficult. This problem is exacerbated when a re-engineering project potentially involves rule recovery from multiple programs in multiple languages. This paper reviews the uses of mathematically formal approaches to business rule recovery and extraction. The applications of provable transformations from different programming languages to Wide Spectrum Language (WSL) are reviewed, and a simple framework for two different rule extraction approaches using WSL is presented. An example of rule extraction using each approach is presented, and the requirements, advantages, and limitations of each approach are examined.