Model reformulation plays an important role in improving models and reducing search space so that solutions can be found faster. In solving Constraint Satisfaction Problems (CSPs), a model of a CSP may be solved rapidly, while a different model may take excessively long to solve. The efficient solution of CSP is significant in real-world applications, such as air traffic management, resource allocation, production scheduling, and bioinformatics. Many technologies such as constraint programming (CP), hybrid technologies, mixed integer programming (MIP), constraint-based local search (CBLS), boolean satisfiability (SAT) could have different solvers and backends to solve the real-time problems. Model reformulation can have a significant impact on solving time. Techniques from formal methods will be used to provide machine assistance for MiniZinc, which is the high-level modelling language to model CSPs. The verification tool, Isabelle, will be used to verify the correctness of reformulations. We plan to apply recent results in formal methods such as program analysis and synthesis to provide semi-automated frameworks for model analysis. In this paper, we identify the challenges, implement frameworks, and evaluate our experimental results in reformulations for future research.