We are currently implementing a business process management solution by
customizing an ERP application. Natural language requirements are entered
as development work items in TFS.  There is an opportunity to increase the
rigor of the formal specification.

*  Is there an approach to reverse engineer a system specification of a
tool (such as Dynamics AX)?
*  Is there a formal process to discover the accumulated technical debt in
a given implementation?

These questions are somewhat high-level and I'd be glad to obtain any
inputs that will help me incrementally advance to the next step (using
OCaml as a formal method).

Thanks,

Ramu