# Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs

arXiv: https://arxiv.org/abs/2501.12972 · HTML: https://mlsanity.com/paper/2501.12972/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 13 of its 31 references that are in the map.
- First posted on arXiv 22 Jan 2025.

## Builds on (most cited first, 13 of 13)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [PICARD: Parsing Incrementally for Constrained Auto-Regressive Decoding from Language Models](https://mlsanity.com/paper/2109.05093/) (2021)
- [Synchromesh: Reliable code generation from pre-trained language models](https://mlsanity.com/paper/2201.11227/) (2022)
- [Jigsaw: Large Language Models meet Program Synthesis](https://mlsanity.com/paper/2112.02969/) (2021)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://mlsanity.com/paper/2407.03203/) (2024)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification](https://mlsanity.com/paper/2305.14752/) (2023)
- [Optimal Neural Program Synthesis from Multimodal Specifications](https://mlsanity.com/paper/2010.01678/) (2020)
- [AI Coders Are Among Us: Rethinking Programming Language Grammar Towards Efficient Code Generation](https://mlsanity.com/paper/2404.16333/) (2024)

## Abstract (arXiv)

When blockchain systems are said to be trustless, what this really means is that all the trust is put into software. Thus, there are strong incentives to ensure blockchain software is correct -- vulnerabilities here cost millions and break businesses. One of the most powerful ways of establishing software correctness is by using formal methods. Approaches based on formal methods, however, induce a significant overhead in terms of time and expertise required to successfully employ them. Our work addresses this critical disadvantage by automating the creation of a formal model -- a mathematical abstraction of the software system -- which is often a core task when employing formal methods. We perform model synthesis in three phases: we first transpile the code into model stubs; then we "fill in the blanks" using a large language model (LLM); finally, we iteratively repair the generated model, on both syntactical and semantical level. In this way, we significantly reduce the amount of time necessary to create formal models and increase accessibility of valuable software verification methods that rely on them. The practical context of our work was reducing the time-to-value of using formal models for correctness audits of smart contracts.