For now, please refer to master's project for the exploration of how Alloy tools are used to verify the safety of Domain Relational Calculus queries.
More updates coming soon.
All software in this project apart from those inside master's project is released under Apache License 2.0.