{"id":"42123e72-1722-4462-8263-e33241999bab","arxiv_id":"2507.16276","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":4.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper presents a multi-level finite state machine model for generating smart contracts from clause automata using reusable packages and reports a security scan with no detected vulnerabilities.","lead":"This paper proposes a multi-level finite state machine model to represent smart contract clauses and automatically generate blockchain program code from them. The authors argue that this hierarchy, built from reusable packages and inter-clause dependencies, makes contract development easier for non-programmers and produces contracts that pass security scans.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Security claim hinges on unverified composition safety: §5 audits packages in isolation but never shows the generator's wiring of guards, state updates, and cross-automaton calls preserves that safety.","rationale":"The reader's conditional verdict is appropriate. The strongest version of the paper's central claim is that a non-specialist can go from clause-level automata to deployable, secure contracts. For that to hold, the generation engine must not introduce vulnerability classes when it composes independently safe package functions into state machines and cross-contract dependencies. This is precisely the premise in §5, and it is neither proven nor empirically supported beyond an unspecified SmartBugs run. I focus on this rather than the manual clause transposition in §4.2 because transposition errors are modeling errors that a reviewer could detect, whereas composition failures are latent and are exactly the bugs that would defeat a non-specialist user. A targeted adversarial FSM with a reentrancy-prone package call would test the engine's wiring; if it produces a vulnerable contract, the security claim in §5 is false for the general method, not just for the tested examples. Since the paper already lacks artifacts and this concern is addressable with a small release plus a test suite, the overall verdict remains CONDITIONAL rather than moving to REJECT.","tokens_in":124,"tokens_out":3611,"duration_ms":52409,"concrete_test":"Request the generator and the exact FSM specifications and generated contracts used in §5, then feed the engine a deliberately adversarial FSM: Clause A's transition guard is a package function that calls an external function in Clause B's automaton, and Clause B's corresponding function performs a state update after the external call. Compile with solc 0.8.29 and run Slither, Mythril, and SmartBugs, plus a functional reentrancy exploit test. If a vulnerability appears, the composition-safety assumption is false; if no vulnerability appears across a suite of such adversarial FSMs, the concern is weakened. Also re-run the original §5 test set from the released artifact to confirm reproducibility.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim that non-specialists can produce secure contracts depends on the premise in §5: 'prior to using the generator, all functions, variables, and structures sourced from established packages were thoroughly audited to ensure their integrity and security.' This treats safety as a property of isolated packages, but the generator's core operation is composition: it maps FSM transitions to guards, state updates, and inter-automaton conditions such as automata__a0_iscompleted (Listing 1), and emits multiple dependent contracts in topological order. Safe components can become unsafe when composed: a package condition function with an external call can reenter a state-changing function before the state update is committed, and two automata with cross-contract completion conditions can create transaction-ordering or access-control flaws even if each clause alone is clean. The paper supplies no invariant, no compositionality argument, and no artifact; §5 only reports that SmartBugs found 'none of these vulnerabilities were present in the generated smart contracts' on unspecified test contracts. That result, if reproducible, speaks to those specific contracts, not to the general claim that the generation engine cannot introduce vulnerabilities. The manual clause-to-FSM step in §4.2 is a separate limitation, but the security claim fails first at the composition step.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":7068,"tokens_out":3844,"duration_ms":39064,"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":[{"comment":"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.","section":"Section 5, Security analysis"},{"comment":"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.","section":"Section 4.2, Contractual Clauses Transposition to FSM Representation"},{"comment":"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.","section":"Section 4.3, Generation Engine and Smart Contract Compilation"},{"comment":"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.","section":"Section 5, Security analysis"}],"minor_comments":[{"comment":"The phrase 'to identify any security flaws' appears twice in consecutive sentences; one copy should be deleted.","section":"Section 5, Security analysis"},{"comment":"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.","section":"Sections 4.3 and 5"},{"comment":"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.","section":"Section 3, Multi-Level Representation"},{"comment":"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.","section":"Listing 1"},{"comment":"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.","section":"Section 1, Introduction"}],"recommendation":"major_revision","confidential_remarks":"To the editor: this manuscript is essentially a tool-design description whose stated empirical claims far exceed the provided evidence. The authors would need to release the generator, the generated test contracts, and the SmartBugs outputs to make the security conclusion credible. If the journal's policy permits tool papers without artifacts, that policy should be explicitly disclosed to referees; otherwise, artifact submission should be a condition for further consideration. The paper is not suitable for acceptance in its current form, but the underlying modeling idea may be salvageable with a substantial revision that narrows the claims and supplies reproducible evidence."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"This one is a system proposal with a clear idea and almost no supporting evidence. The new bit is combining hierarchical (multi-level) FSMs with reusable JSON package libraries for Solidity generation. That is a modest extension of what VeriSolid and Symboleo already do with flat or specification-level state machines, and the authors cite those tools honestly. The paper's structure is readable, the pipeline from FSM specification to code with topological ordering is described coherently, and they are upfront that clause-to-FSM transposition is currently manual, which undercuts the automation claim but counts in their favor for candor.\n\nThe soft spots are real and load-bearing. First, there is no artifact: no released code, no generated contract listing, no test suite, no benchmark. The SmartBugs security analysis is described in a few sentences with no details about how many contracts were generated, what they contained, or what exact tools and configurations were used. That makes the headline claim — that the generator produces contracts free of common vulnerability classes — unverifiable from the paper alone. The stress-test note about compositionality is the sharper version of the same problem: even if every package function is audited in isolation, the generator's wiring of guards, state updates, and cross-automaton conditions is exactly where new vulnerabilities could be introduced; no invariant or compositionality argument is offered. So the security claim, as stated, only speaks to those specific test contracts, not to the general approach.\n\nA secondary issue is the manual transcription step. Until that is automated, the tool is not really \"from contracts to code\" for non-programmers; it is a structured way for programmers to encode FSMs. The paper also offers no comparison against existing tools like VeriSolid or Caterpillar, so it is hard to see what concrete advantage the hierarchy buys in practice.\n\nNone of this is fatal to the research direction. The model is plausible, the package idea has merit, and the gaps are addressable with released code and a proper evaluation. But the paper as submitted is more of a position statement than a verified contribution. I would not cite it yet, but I would send it to a serious referee if the authors can provide an artifact. As it stands, it deserves a major-revision-or-reject verdict, not desk rejection, because the underlying problem — accessible and trustworthy smart contract generation — matters.","headline":"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.","tokens_in":7588,"tokens_out":1777,"would_cite":false,"duration_ms":20924,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["smart contracts","multi-level finite state machine","code generation","blockchain","security analysis","Solidity","reusable packages","modularity"],"falsifier":"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.","tokens_in":6655,"feed_emoji":"⚙️","tokens_out":7181,"duration_ms":65310,"temperature":0.7,"pith_summary":"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.","feed_headline":"Finite-state machines turn contract clauses into audited Solidity code","feed_subtitle":"A multi-level FSM pipeline generates modular contracts that pass a 20-tool security scan for common vulnerabilities.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Establishes the smart-contract concept that the paper's automatic generation pipeline is built to deliver.","marker":"[15]"},{"why":"Defines the Ethereum platform that is the paper's initial compilation and deployment target.","marker":"[2]"},{"why":"Supplies the consolidated 20-tool execution framework used in the security analysis.","marker":"[6]"},{"why":"Supplies the FSM-based contract generation approach the paper builds on and contrasts with.","marker":"[8]"},{"why":"Supplies the model-driven business-process-to-Solidity baseline against which the multi-level FSM approach is positioned.","marker":"[10]"},{"why":"Supplies state-machine synthesis case studies that motivate the automaton-per-clause modeling of contracts.","marker":"[12]"},{"why":"Supplies the legal-contract specification-language comparison for the proposed modeling approach.","marker":"[13]"},{"why":"Defines the catalogue of Ethereum smart contract attacks whose absence the security analysis checks.","marker":"[1]"}],"fun_headline_variants":["Multi-level FSMs turn contract pages into Solidity","Automating smart contract coding with layered automata","From clause automata to audited contracts, no Solidity","Hierarchical FSMs generate secure contracts from clauses","Clause-level automata produce modular Solidity code"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Multi-level FSMs turn contract pages into Solidity","Automating smart contract coding with layered automata","From clause automata to audited contracts, no Solidity","Hierarchical FSMs generate secure contracts from clauses","Clause-level automata produce modular Solidity code"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000158,"raw_usage":{"total_tokens":1211,"prompt_tokens":915,"completion_tokens":296,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":531,"completion_tokens_details":{"reasoning_tokens":220}},"tokens_in":531,"tokens_out":296,"duration_ms":4054,"temperature":1.0,"reasoning_tokens":220,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T15:13:34.487995+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Establishes the smart-contract concept that the paper's automatic generation pipeline is built to deliver."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines the Ethereum platform that is the paper's initial compilation and deployment target."},{"cited_title":"di Angelo, T","cited_arxiv_id":null,"evidence_quote":"Supplies the consolidated 20-tool execution framework used in the security analysis."},{"cited_title":"VeriSolid: Correct-by-Design Smart Contracts for Ethereum","cited_arxiv_id":"1901.01292","evidence_quote":"Supplies the FSM-based contract generation approach the paper builds on and contrasts with."},{"cited_title":"CATERPILLAR: A Business Process Execution Engine on the Ethereum Blockchain","cited_arxiv_id":"1808.03517","evidence_quote":"Supplies the model-driven business-process-to-Solidity baseline against which the multi-level FSM approach is positioned."},{"cited_title":"Smart Contract Design Meets State Machine Synthesis: Case Studies","cited_arxiv_id":"1906.02906","evidence_quote":"Supplies state-machine synthesis case studies that motivate the automaton-per-clause modeling of contracts."},{"cited_title":"A survey of attacks on ethereum smart contracts (SOK),","cited_arxiv_id":null,"evidence_quote":"Defines the catalogue of Ethereum smart contract attacks whose absence the security analysis checks."}],"review_version":1}