In this article, we describe the process of generating smart contract code using AI-driven tools and its subsequent verification via the insertion modeling system. Initially, we outline the process of defining and specifying smart contract requirements, the creation of acceptance criteria in the Gherkin language. Next, we generated the smart contract code in the Solidity language based on delineated requirements using AI. The contract`s purpose is to manage the token unlocking processes for decentralized platform investors. We describe the process of translating the smart contract code into the algebraic specifications of the IMS system through ANTLR grammar. To ensure the functional correctness of smart contract operations, we formalized the acceptance criteria described in the goal state syntax and checked whether the smart contract code reaches the goal state defined in the requirements specification. The study shows how these techniques can improve the quality and reliability of smart contracts in distributed systems. The described approach allows us to check the correctness of the smart contract’s functioning logic and its compliance with the given specifications.