Pith. sign in

REVIEW 4 major objections 5 minor 18 references

From Contracts to Code: Automating Smart Contract Generation with Multi-Level Finite State Machines

T0 review · 4 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Smart contracts can be generated from clause-level automata, and the paper reports that the resulting Solidity passes a 20-tool security scan with none of the common vulnerability classes present.

desk verdict A plausible design for hierarchical FSM-based smart contract generation, but no artifacts, no evaluation, and an unverifiable security claim make it a conditional proposal at best. read the letter →

arxiv 2507.16276 v1 pith:ISSPQ6P6 submitted 2025-07-22 cs.CR

Lambard Maxence , Bertelle Cyrille , Duvallet Claude This is my paper · ORCID
classification cs.CR
keywords smartcontractsmulti-levelfinitestatemachinecodegenerationblockchainsecurityanalysisSolidityreusablepackagesmodularity
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper claims that a multi-level finite state machine model can lower the barrier to smart contract development: a contract's clauses are first represented as automata, and a generation engine turns that representation into deployable Solidity code. Because each clause is its own machine and transitions can be guarded by conditions coming from package functions or from other clause automata, the model is said to give modularity, traceability, and dynamic inter-clause dependencies. The authors report that generated test contracts passed a 20-tool security analysis with none of the common vulnerability classes present. A sympathetic reader would care because, if the claim holds, professionals without programming expertise could produce contracts that are both executable and auditable rather than hand-written code requiring expert review.

What carries the argument

The central mechanism is the multi-level finite state machine: each contract clause is a small automaton with states and transitions, and each transition is labeled by a trigger and a set of conditions; conditions can be package functions or completion predicates of other automata, creating a hierarchy of interconnected machines. The supporting machinery is a package library in JSON format containing pre-developed, audited functions, variables, and structures, plus a generation engine that checks the FSM specification, generates the Solidity contracts in topological order to avoid cyclic dependencies, formats the code, and runs a security audit. This machinery is what carries the paper's modularity and traceability claims, since each clause remains an independently readable automaton while its dependencies on other clauses are explicit.

What would settle it

Generate a corpus of FSM specifications with inter-clause dependencies, run the 20-tool vulnerability suite on the resulting Solidity, and look for any of the nine listed weakness classes; a single hit in any generated contract would refute the paper's claim that none of these vulnerabilities were present.

Watch

Extended reading notes

Core claim

The paper's central claim is that a multi-level finite state machine representation, together with reusable package libraries and a generation engine, is sufficient to produce modular, traceable smart contracts from clause-level automata. Each clause is modeled as an automaton whose transitions are guarded by conditions, and those conditions may refer to functions supplied by audited packages or to the completion of other clause automata, which is how inter-clause dependencies are represented. A generation engine verifies the FSM specification, constructs the contracts in topological order, compiles and deploys them, and the authors report that a consolidated 20-tool vulnerability scan found none of the commonly studied vulnerability classes in the generated test contracts. The paper's model is therefore put forward as a path for non-specialists to obtain secure, executable contracts without writing Solidity directly.

Load-bearing premise

The security claim rests on the assumption that the pre-audited package functions, variables, and structures remain safe when the generation engine wires them into new state-and-transition structures (Section 5), and that natural-language clauses can be faithfully transposed into FSM specifications (Section 4.2); if either gives way, the generated contracts may be insecure or unfaithful even when they compile and scan cleanly.

Editorial extensions

If this is right

  • Non-specialists can go from a clause-level FSM specification to a deployable, compilable smart contract without writing Solidity by hand.
  • Each contract clause remains an identifiable automaton in the final code, so execution can be monitored state-by-state and traced back to the original clause.
  • Inter-clause dependencies are first-class, expressed as completion conditions of other automata, while a topological generation order rules out cyclic dependency between clauses.
  • Reusable, audited package components keep contracts modular across projects, so updates and new contracts can be assembled rather than rewritten.
  • If the security analysis is representative, the generated contracts avoid reentrancy, integer overflow, unchecked low-level calls, Tx.origin issues, time manipulation, delegate call, access control, transaction-ordering dependence, and denial of service.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Going beyond the paper: the real fidelity risk sits in the manual transposition of natural-language clauses into FSM specifications (Section 4.2), so an automated transposition step with a faithfulness measure would be the natural next test.
  • Going beyond the paper: the security result is conditional on the package-audit premise in Section 5; a stress test that deliberately combines non-audited or adversarial package functions would reveal whether the generation engine itself introduces vulnerabilities when wiring states and transitions.
  • Going beyond the paper: because the FSM specification and packages are backend-agnostic, the same pipeline could target other blockchains by swapping only the compilation and deployment layer, which would test the portability claim.
  • Going beyond the paper: generated contracts could be compared against hand-written reference implementations on the same clauses to quantify whether the automaton model loses any contractual semantics in translation.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. This paper presents a method for generating Ethereum smart contracts from a multi-level finite state machine (FSM) representation. The authors propose that each contractual clause is modeled as an automaton, that reusable package libraries supply functions, variables, and structures, and that a generation engine compiles the FSM specification into Solidity code. The paper claims that the approach simplifies contract development for non-specialists, enhances modularity and traceability, and produces secure contracts, reporting a SmartBugs-based security analysis that found none of nine common vulnerability classes in generated contracts. The authors explicitly acknowledge that the clause-to-FSM transposition is currently performed manually, and they list a future Visual Programming Language as next work.

Significance. If the result holds, the contribution is practically relevant: it offers a higher-level abstraction than raw Solidity and targets a known barrier to smart contract adoption, namely the need for deep programming expertise. The paper's strengths are the clear architectural sketch of package libraries and the planned use of an existing vulnerability-detection framework (SmartBugs) for output checking. However, the manuscript contains no generated code, no test artifacts, no tool outputs, and no formal or machine-checked proof of the claimed properties; the only executable evidence is a one-sentence assertion that a SmartBugs scan found no vulnerabilities. The central claims are therefore plausible but currently unsupported, and the absence of reproducibility artifacts is a major shortcoming for a systems-oriented paper.

major comments (4)
  1. [Section 5, Security analysis] The headline claim that 'none of these vulnerabilities were present in the generated smart contracts' is not verifiable from the manuscript: no generated contracts, test configurations, or SmartBugs outputs are included. More importantly, the assertion that pre-audited package components guarantee security assumes compositional safety. The generation engine maps FSM transitions to guards, state updates, and cross-automaton conditions (e.g., automata__a0_iscompleted in Listing 1) and emits dependent contracts in topological order, yet the authors provide no invariant or compositionality argument showing that wiring audited functions together cannot introduce reentrancy, access-control, or transaction-ordering flaws. This is a load-bearing gap because the security guarantee is a central advertised contribution.
  2. [Section 4.2, Contractual Clauses Transposition to FSM Representation] The manuscript explicitly states that contractual clauses are 'currently manually transposed into a finite state machine (FSM) representation.' This manual step is part of the generation pipeline, so the claimed automation from natural-language contracts to code is not achieved. Furthermore, no evidence is given that the FSM faithfully preserves the semantics of the original contractual clauses; if clause semantics are lost in transposition, the generated contract does not implement the intended agreement even if it passes security scans. The authors should either scope the automation claim to inputs already expressed as FSMs or provide a validated method for the transposition.
  3. [Section 4.3, Generation Engine and Smart Contract Compilation] The engine's core step, 'converting states and transitions into executable code,' is described only at a high level; no algorithm, template, mapping rule, or pseudocode is given, and no generated Solidity code is shown anywhere in the paper. Listing 1 demonstrates an input FSM specification, but the corresponding output contract is never presented. Without a concrete input/output example, the central mechanism of the paper is unsubstantiated, and a reader cannot assess the correctness of the generated code or the actual degree of automation.
  4. [Section 5, Security analysis] The empirical description is too thin to support the security conclusion: the paper does not report the number of test contracts, the size or complexity of the contracts, which specific tools within SmartBugs were run, or any raw outputs or severity counts. The single sentence reporting the absence of vulnerabilities is an aggregate assertion that cannot be reproduced or checked. Even if the compositionality concern were resolved, this lack of detail would prevent the security claim from being considered evidence.
minor comments (5)
  1. [Section 5, Security analysis] The phrase 'to identify any security flaws' appears twice in consecutive sentences; one copy should be deleted.
  2. [Sections 4.3 and 5] The paper states that a generation engine was developed and that test contracts were generated, but it provides no repository, artifact URL, or executable package under the authors' control. A public artifact is essential for verifiability and for the security claim to be credibly evaluated.
  3. [Section 3, Multi-Level Representation] Figure 1 is referenced as showing interactions among clauses, but the multiple hierarchy levels are not labeled in the textual description; please add explicit level annotations to the figure so the 'multi-level' aspect is visually and textually unambiguous.
  4. [Listing 1] The JSON keys appear with leading spaces (e.g., ' Clause A ', ' t r a n s i t i o n s '), which is a likely formatting artifact; the listing should show the actual JSON keys without extraneous spaces.
  5. [Section 1, Introduction] The introduction claims the multi-level architecture 'guarantees optimized performance' and 'guarantees total transparency,' but no performance or transparency evaluation is provided; please temper these claims or add measurements.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: the proposal is stated, not derived, and the security claim rests on external tools and explicitly stated audit assumptions.

full rationale

The paper does not present a derivation chain in which an output is equivalent to its input by construction. The core contribution, mapping an FSM specification (Listing 1) through a generation engine to Solidity code, is described procedurally rather than derived. The security claim in Section 5 is an empirical report using the external SmartBugs framework: "Our analysis revealed that none of these vulnerabilities were present in the generated smart contracts." The pre-audit of package components is stated as an explicit assumption, "prior to using the generator, all functions, variables, and structures sourced from established packages were thoroughly audited to ensure their integrity and security," not as a consequence of the model. The manual clause-to-FSM transposition in Section 4.2 is acknowledged as manual, so there is no hidden self-referential fit. I found no self-citations bearing on the central claim, no fitted parameters renamed as predictions, and no uniqueness theorem imported from the authors' prior work. The identified limitations, such as unproven composition safety of packages, unspecified test contracts, and the manual clause-to-FSM step, are evidential or soundness gaps rather than circularity. Therefore the appropriate circularity score is 0.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

No numeric parameters are fitted or hand-tuned in this paper. The model's behavior is defined by state and transition specifications and package functions, not by scalar constants. The multi-level FSM model is a software modeling construct rather than a physical or formal entity, so no ontology entries are added.

assumptions (4)
  • domain assumption Every contractual clause can be faithfully represented as a finite state machine with states and transitions.
    Section 3 and Listing 1 assume this transposition; clause semantics that do not fit a state/transition structure would be distorted or lost.
  • domain assumption All relevant transition guards are expressible as package functions or as completion of other automata.
    Listing 1 and Section 4.1 use only these two condition types without a completeness argument.
  • domain assumption Audited package components remain secure when composed by the generation engine.
    Section 5 states packages were 'thoroughly audited' and then infers the generated contracts have none of the common vulnerabilities; component-wise security is assumed to compose without proof.
  • domain assumption Generating contracts in topological order is sufficient to avoid cycles and preserve dependency semantics.
    Section 4.3 mentions topological order and Section 5 asserts cyclic dependencies are impossible, but the actual ordering rule and its correctness are not specified.

how reviews work

0 comments
Cite this review

Pith. "Pith review of From Contracts to Code: Automating Smart Contract Generation with Multi-Level Finite State Machines." pith.science (2026). https://pith.science/paper/ISSPQ6P6

@misc{pith2026250716276,
  author       = {Pith},
  title        = {Pith review of: From Contracts to Code: Automating Smart Contract Generation with Multi-Level Finite State Machines},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ISSPQ6P6}},
  note         = {Machine review of arXiv:2507.16276}
}
read the original abstract

In an increasingly complex contractual landscape, the demand for transparency, security, and efficiency has intensified. Blockchain technology, with its decentralized and immutable nature, addresses these challenges by reducing intermediary costs, minimizing fraud risks, and enhancing system compatibility. Smart contracts, initially conceptualized by Nick Szabo and later implemented on the Ethereum blockchain, automate and secure contractual clauses, offering a robust solution for various industries. However, their complexity and the requirement for advanced programming skills present significant barriers to widespread adoption. This study introduces a multi-level finite state machine model designed to represent and track the execution of smart contracts. Our model aims to simplify smart contract development by providing a formalized framework that abstracts underlying technical complexities, making it accessible to professionals without deep technical expertise. The hierarchical structure of the multi-level finite state machine enhances contract modularity and traceability, facilitating detailed representation and evaluation of functional properties. The paper explores the potential of this multi-level approach, reviewing existing methodologies and tools, and detailing the smart contract generation process with an emphasis on reusable components and modularity. We also conduct a security analysis to evaluate potential vulnerabilities in our model, ensuring the robustness and reliability of the generated smart contracts.

Figures

Figures reproduced from arXiv: 2507.16276 by the authors.

Figure 1
Figure 1. Multi-level representation. Unlike classical finite state machines, which operate on a single level of abstraction, the multi-level approach is based on a hierarchy of intercon￾nected finite state machines. At each level, a finite state machine controls the transitions of a global process, while sub-machines detail more specific processes. This structure allows for dynamic dependencies between contract 5 [PITH_FULL… view at source ↗
Figure 2
Figure 2. Generation and deployment processes [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Simple clauses representation. 8 [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Dependency graph of test contract with clause 2 detailed. [PITH_FULL_IMAGE:figures/full_fig_p012_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

18 extracted references · 16 canonical work pages

  1. [1]

    A survey of attacks on ethereum smart contracts (SOK),

    N. Atzei, M. Bartoletti, and T. Cimoli, “A survey of attacks on ethereum smart contracts (SOK),” in Princ. Secur. Trust: 6th Int. Conf., Uppsala, Sweden, Springer, 2017, pp. 164–186

    work page 2017

  2. [2]

    V. Buterin. Ethereum: A Next-Generation Smart Con- tract and Decentralized Application Platform. 2014, https://ethereum.org/en/whitepaper/

    work page 2014

  3. [3]

    From Institutions to Code: To- wards Automated Generation of Smart Contracts

    C. Frantz, and M. Nowostawski. “From Institutions to Code: To- wards Automated Generation of Smart Contracts.” 2016 IEEE 1st In- ternational Workshops on Foundations and Applications of Self* Sys- tems (F AS*W), IEEE, 2016, pp. 210–15, https://doi.org/10.1109/F AS- W.2016.53

    work page doi:10.1109/f 2016

  4. [4]

    Towards Model-Driven Engineering of Smart Contracts for Cyber-Physical Systems

    P. Garamvolgyi, and al. “Towards Model-Driven Engineering of Smart Contracts for Cyber-Physical Systems.” 2018 48th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Work- shops (DSN-W), IEEE, 2018, pp. 134–39,https://doi.org/10.1109/DSN- W.2018.00052

    arXiv 2018

  5. [5]

    A Systematic Review and Performance Evaluation of Open-Source Tools for Smart Contract Vulnerability Detection

    Y. He, and al. “A Systematic Review and Performance Evaluation of Open-Source Tools for Smart Contract Vulnerability Detection.” Com- puters, Materials and Continua, vol. 80, no. 1, 2024, pp. 995-1032, https://doi.org/10.32604/cmc.2024.052887

    work page arXiv 2024

  6. [6]

    di Angelo, T

    M. di Angelo, T. Durieux, J. F. Ferreira, Gernot Salzer: ”SmartBugs 2.0: An Execution Framework for Weakness Detection in Ethereum Smart Contracts”, in Proc. 38th IEEE/ACM International Conference on Au- tomated Software Engineering (ASE), pages 2102-2105, IEEE Computer Society, 2023

    work page 2023

  7. [7]

    A survey on the secu- rity of blockchain systems,

    X. Li, P. Jiang, T. Chen, X. Luo, and Q. Wen, “A survey on the secu- rity of blockchain systems,” Future Gen. Comput. Syst., vol. 107, pp. 841–853, 2020. https://10.1016/j.future.2017.08.020

    work page doi:10.1016/j.future.2017.08.020 2020

  8. [8]

    VeriSolid: Correct-by-Design Smart Contracts for Ethereum

    A. Mavridou, and al. VeriSolid: Correct-by-Design Smart Contracts for Ethereum. arXiv, 2019, https://doi.org/10.48550/ARXIV.1901.01292. 14

    work page Pith review arXiv doi:10.48550/arxiv.1901.01292 2019

Show all 18 references
  1. [9]

    Nakamoto

    S. Nakamoto. Bitcoin: A Peer-to-Peer Electronic Cash System. 2008, https://bitcoinwhitepaper.co/bitcoin.pdf

    2008

  2. [10]

    L´ opez-Pintado, Orlenys, and al

    O. L´ opez-Pintado, Orlenys, and al. CATERPILLAR: A Business Pro- cess Execution Engine on the Ethereum Blockchain. arXiv, 2018, https://doi.org/10.48550/ARXIV.1808.03517

    2018 doi arXiv

  3. [11]

    Das Contract - A Visual Domain Specific Language for Modeling Blockchain Smart Contracts

    M. Skotnica and R. Pergl. “Das Contract - A Visual Domain Specific Language for Modeling Blockchain Smart Contracts.” Ad- vances in Enterprise Engineering XIII, edited by David Aveiro et al., vol. 374, Springer International Publishing, 2020, pp. 149–66, https://doi.org/10.100...

    2020 doi

  4. [12]

    Suvorov and V

    D. Suvorov and V. Ulyantsev. Smart Contract Design Meets State Machine Synthesis: Case Studies. arXiv, 2019, https://doi.org/10.48550/ARXIV.1906.02906

    2019 doi arXiv

  5. [13]

    Symboleo: Towards a Specification Lan- guage for Legal Contracts

    S. Sharifi, and al. “Symboleo: Towards a Specification Lan- guage for Legal Contracts.” 2020 IEEE 28th International Re- quirements Engineering Conference (RE), IEEE, 2020, pp. 364–69, https://doi.org/10.1109/RE48521.2020.00049

    2020

  6. [14]

    The Development of Smart Contracts for Heterogeneous Blockchains

    H. Syahputra, and H. Weigand. “The Development of Smart Contracts for Heterogeneous Blockchains.” Proceedings of the I-ESA’18 Confer- ence, edited by K. Popplewell et al., Springer Verlag, 2019, pp. 229–38, https://doi.org/10.1007/978-3-030-13693-2 19

    2019 doi

  7. [15]

    N. Szabo. Smart Contracts: Building Blocks for Digital Markets. 1996, http://www.truevaluemetrics.org/DBpdfs/BlockChain/Nick-Szabo- Smart-Contracts-Building-Blocks-for-Digital-Markets-1996-14591.pdf

    1996

  8. [16]

    Automatic Smart Contract Generation Us- ing Controlled Natural Language and Template

    T. Tateishi, and al. “Automatic Smart Contract Generation Us- ing Controlled Natural Language and Template.” IBM Journal of Research and Development, vol. 63, no. 2/3, 2019, p. 6:1-6:12, https://doi.org/10.1147/JRD.2019.2900643

    2019

  9. [17]

    Lorikeet: A Model-Driven Engineering Tool for Blockchain-Based Business Process Execution and Asset Management

    A. B. Tran, and al. “Lorikeet: A Model-Driven Engineering Tool for Blockchain-Based Business Process Execution and Asset Management.” CEUR Workshop Proceedings, vol. 2196, 2018, pp. 56–60. 15

    2018

  10. [18]

    Data security and privacy in bitcoin system: A survey,

    L. Zhu, B. Zheng, M. Shen, F. Gao, H. Li and K. Shi, “Data security and privacy in bitcoin system: A survey,” J. Comput. Sci. Technol., vol. 35, no. 4, pp. 843–862, 2020. https://doi.org/10.1007/s11390-020-9638-7. 16

    2020 doi

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.