Abstract: Formal description and formal verification methods are used to develop the first smart legal contract for digital currencies tailored to multi-party application scenarios. A domain specific language model(DSLM) adapted to digital currency transactions was designed. A multi-party interaction temporal model based on computational tree logic and linear temporal logic(LTL), precisely described the execution sequence of transactions, the interaction behaviors of participating parties, and the legal obligations and responsibilities of all parties during the transaction process. An automated smart contract code generation scheme was designed, which can automatically convert the transaction logic and temporal model described in the DSLM into smart contract code, significantly improving the efficiency of smart contract development while reducing human involvement and potential coding errors. All above is applied in the business instance of enterprise loans:a scenario involving multiple contracts and interactions among various parties, and the result shows that the smart legal contract for digital currencies can reflect business needs accurately and demonstrates excellent efficiency and legal compliance in the multi-party application scenario.