Formal Verification

A bridge specifies that finalized withdrawals cannot mint more destination tokens than locked source value under its model. The team seeks exhaustive assurance for that property. What discipline applies?