Comparative Analysis of Solidity Smart Contract Generation Using Large Language Models Based on Formal Algebraic Specifications

2025;
: pp. 229 - 243
1
Kherson State University, Department of Computer Science and Software Engineering, Kherson, Ukraine
2
Kherson State University, Department of Computer Science and Software Engineering, Kherson, Ukraine

This article presents a comparative analysis of automatic Solidity smart contract generation using large language models (LLMs) based on two approaches: natural language textual descriptions and formal algebraic specifications. The study analyzes smart contracts generated by LLMs (ChatGPT-4, Claude 3.7 Sonnet, DeepSeek-V3) as well as by the AI-based tool GitHub Copilot, evaluating their syntactic correctness, compliance with initial requirements, and security. The security of the smart contracts was assessed through static analysis using the Slither tool to identify potential vulnerabilities, including reentrancy attacks and arithmetic overflows.

To create the formal specification, we applied the Insertion Modeling System (IMS), which enables formal descriptions of smart contract behavior using algebraic specifications. To improve the interpretation of these specifications by large language models, we proposed a few-shot prompting approach, which involves providing LLM with demonstration examples of algebraic specifications and the corresponding Solidity code to improve the interpretation of formal models. The proposed approach allowed us to increase the accuracy of translating formal specifications into code, reduce the number of syntax errors, and ensure better compliance with the original model.

The study found that natural language prompts are easier to use for quick code generation but are less reliable, as their inherent ambiguity tends to produce hidden vulnerabilities. In contrast, formal models require additional effort to guide the LLM and eliminate interpretation errors, but they allow for a much more accurate representation of contract logic, resulting in higher-quality generation of contracts with complex behavior.

  1. Bergmann, D. (2024). Context window. IBM.com. https://www.ibm.com/think/topics/context-window
  2. Chatterjee, S., Ramamurthy, B. (2025). Efficacy of Various Large Language Models in Generating Smart Contracts. In: Arai, K. (eds) Advances in Information and Communication. FICC 2025. Lecture Notes in Networks and Systems, vol 1284. Springer, Cham. https://doi.org/10.1007/978-3-031-85363-0_31
  3. Cleary, D. (2025). In Context Learning Guide. PromptHub. https://www.prompthub.us/blog/in-context-learning-guide Crytic. Slither static analysis framework. GitHub. https://github.com/crytic/slither
  4. Fadi, B., Napoli, E. A., Gatteschi, V., & Schifanella, C. (2024). Automatic Smart Contract Generation Through LLMs: When The Stochastic Parrot Fails. In Proceedings of DLT 2024. CEUR.
  5. Fravoll. Checks, Effects, Interactions pattern in Solidity. (2025) https://fravoll.github.io/solidity- patterns/checks_effects_interactions.html
  6. Kang, I., Woensel, W. V., & Seneviratne, O. (2024). Using Large Language Models for Generating Smart Contracts for Health Insurance from Textual Policies. In AI for Health Equity and Fairness (pp. 129–146). Springer. https://doi.org/10.1007/978-3-031-63592-2_11
  7. Letichevsky, A., Kapitonova, J., Letichevsky Jr, A., Volkov, V., Baranov, S., & Weigert, T. (2005). Basic protocols, message sequence charts, and the verification of requirements specifications. Computer Networks, 49(5), 661–675. https://doi.org/10.1016/j.comnet.2005.05.005
  8. Letichevsky, A., Letychevskyi, O., & Peschanenko, V. (2016). Insertion modeling and its applications. Computer Science Journal of Moldova, 72(3), 357–370.
  9. Modi, M. (2024). Transforming software development through generative AI: A systematic analysis of automated development practices. International Journal of Scientific Research in Computer Science, Engineering and Information Technology, 10(6), 536–547. https://doi.org/10.32628/cseit24106197
  10. Peschanenko, V., Poltorackiy, M., & Konnova, O. (2025). Verification of Smart Contract Code Generated by Applying Artificial Intelligence. In: Ermolayev, V., et al. Information and Communication Technologies in Education, Research, and Industrial Applications. ICTERI 2024. Communications in Computer and Information Science, vol 2359. Springer. https://doi.org/10.1007/978-3-031-81372-6_1
  11. Prompt Engineering Guide. Few-shot prompting. https://www.promptingguide.ai/techniques/fewshot
  12. Wong, M. F., Guo, S., Hang, C. N., Ho, S., & Tan, C. W. (2023). Natural language generation and understanding of big code for AI-assisted programming: A review. Entropy, 25.