Pith. sign in

REVIEW 3 major objections 5 minor 44 references

Towards LLM-assisted High-Quality Property Generation for Solidity Smart Contracts

T0 review · 3 major / 5 minor · reviewed 2026-07-31 · deepseek-v4-flash

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

Pith's one-line read Gemini Pro 1.5 with prompt chaining generates Solidity test properties that score 25.99% on mutation testing, close to the 31.75% human benchmark.

desk verdict The per-contract LibBit result is credible, but the headline 25.99% average is inflated by best-of-five selection and by silently ignoring non-executable outputs; the paper needs revision before that average claim can be accepted. read the letter →

arxiv 2607.23308 v1 pith:V5YL2Y2U submitted 2026-07-25 cs.SE

Muhammad Wahid , Shahzaib Khan , Mashhood Ali , Muhammad Hassan , Muhammad Naiman Jalil , Affan Rauf This is my paper
classification cs.SE
keywords smartcontractsSolidityproperty-basedtestinglargelanguagemodelsmutationpromptchainingfuzzingsoftware
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

This paper claims that large language models can generate property-based tests for Solidity smart contracts whose bug-detection quality approaches that of human-written tests. Using mutation testing as the yardstick, the best configuration—Gemini Pro 1.5 with prompt chaining—kills 25.99% of mutants on average, versus 31.75% for human tests. On one contract, LibBit, the LLM-generated tests reach 74.34%, nearly matching the human 74.83%. The authors argue that dividing generation into subtasks (list functionalities, list properties in English, convert to Solidity) is key, and that this could reduce the manual effort and cost of property-based testing for blockchain code.

What carries the argument

The central mechanism is prompt chaining: instead of asking an LLM to write tests in one step, the task is split into three chained prompts—explaining each function of the contract, listing test properties in natural language, and converting those properties into Solidity test code. The quality of the generated properties is measured by mutation testing, which applies 44 Solidity-specific mutation operators to the contract, reruns the properties on each mutant, and computes the fraction of mutants killed (mutation score). The paper compares this across three LLMs and three prompting styles, using a human-written test suite as the benchmark.

What would settle it

Recompute average mutation scores counting every non-executable output as 0 (no best-of-five selection, no manual repair), using the same prompts and contracts. If Gemini Pro 1.5 prompt chaining drops far below 25.99% or below the zero-shot baselines, the paper's central claim about approaching human quality is not supported for raw LLM output.

Watch

Extended reading notes

Core claim

The central claim is that state-of-the-art LLMs, prompted in a staged fashion, can produce executable, mutation-killing properties for Solidity smart contracts at a level close to human experts. The evidence is a set of averages across 35 utility contracts: the best configuration, Gemini Pro 1.5 with prompt chaining, achieves 25.99% average mutation score, approaching the 31.75% human baseline, and on the LibBit contract it scores 74.34% versus 74.83% human. The paper treats this as evidence that LLM-assisted property generation is a viable way to lower the cost of pre-deployment testing for smart contracts.

Load-bearing premise

The headline 25.99% mutation score assumes that a property counts as LLM-generated even when the authors selected the best of up to five outputs and manually fixed compilation and logic errors, and that contracts where no output ever became executable can be dropped from the average instead of scored as zero.

Editorial extensions

If this is right

  • If correct, LLM-generated property tests can serve as a low-cost first line of defense for smart contract security, especially for simple utility libraries.
  • Prompt chaining is a readily usable technique that consistently outperforms single-shot generation, suggesting that decomposition helps LLMs produce better tests.
  • The LibBit result indicates that for some contracts, LLM output is effectively interchangeable with human-written tests, so effort can be redirected to more complex contracts.
  • The high variance across contracts means organizations should use mutation testing or similar validation before trusting generated properties.
  • The approach's success on Solidity suggests it may transfer to other smart-contract languages or to other domains where property-based testing is manual.

Reading between the lines

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

  • If the gap between LLM and human mutation scores continues to close, property-based testing could become a default, automated step in smart contract CI/CD pipelines, not a rare expert activity.
  • The paper's reported average may be optimistic because non-executable outputs are excluded and the best of several LLM outputs is selected; a stricter per-request evaluation would clarify raw model capability and likely lower the headline number.
  • The few-shot approach's poor performance despite higher executability suggests that retrieval quality, not just example presence, is the bottleneck; a larger, domain-matched example bank could boost few-shot results.
  • The authors' manual repair of compilation and logic errors could itself be partially automated by agentic LLM loops, as the paper notes; testing that extension would directly quantify how much human effort remains.
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

3 major / 5 minor

Summary. The paper proposes an LLM-assisted pipeline for generating Foundry property-based tests for Solidity smart contracts, comparing zero-shot, few-shot (2-shot), and prompt-chaining configurations on GPT-4o, GPT-4-Turbo, and Gemini-1.5-pro. The contracts are taken from the Solady utils library, and the generated tests are evaluated by mutation testing using Sumo. The headline claim is that Gemini-1.5-pro with prompt chaining achieves a 25.99% average mutation score, 'closely approaching' the human-written Solady benchmark of 31.75%, with a notable per-contract result for LibBit (74.34% vs. 74.83%). The per-contract evidence is plausible, but the average-level claim is not supported as stated because non-executable outputs are excluded from the average and the pipeline includes best-of-five selection and manual repair.

Significance. If the headline claim were supported, this would be a useful empirical contribution: a systematic comparison of modern LLMs and prompting strategies for generating property-based tests, with mutation score as an external quality metric. The paper's main strengths are the per-contract mutation score table, the LibBit case study, and the candid documentation of concrete failure modes and manual-repair steps in Sections III-F and III-G. There is no parameter fitting or definitional circularity: mutation score is an external measurement. However, the central quantitative claim is currently overstated because the reported average is computed only over executable outputs, while the human baseline averages all contracts. The paper needs a reanalysis and a more careful wording of the 'closely approaching' claim; as it stands, the contribution is better characterized as an existence proof at the individual-contract level.

major comments (3)
  1. [Abstract; Section III-E; Table II; Section IV] The 25.99% headline is an average over non-N/E cells only, whereas the human 31.75% baseline in Table II averages all contracts (except the one marked N/A). In the Gemini prompt-chaining column, 16 of the 34 contracts are marked N/E. If these N/E cells are counted as zero, the column average is approximately 14.5%, not 25.99%, and the claim that the result 'closely approaches' the human benchmark is not supported. Section IV says N/E means non-executable even after 3 to 5 different calls, so excluding these cells is not a neutral missingness decision. The paper should report an intent-to-treat average with N/E as zero, report the denominator for each average, and rephrase the abstract accordingly.
  2. [Section II-A; Section II-C; Section III-F] The reported mutation scores do not measure raw LLM capability. Section II-C says the authors made up to five requests per contract and selected the output with more executable properties; Section II-A says properties are included if they are executable or 'can be made executable with minimal manual effort'; Section III-F documents that compilation errors and logic errors were manually repaired. This may be a legitimate description of an LLM-assisted pipeline, but it must be stated as such. The current wording, e.g., 'Gemini Pro 1.5, when combined with prompt chaining, achieves...', implies an automated method. Please quantify how many outputs/properties were manually repaired, how much effort was involved, and provide an automatic-only score or a clear caveat that the 25.99% figure includes human intervention and best-of-five selection.
  3. [Table II; Section III-E] The per-contract results show very high variance and many zero or near-zero scores, which makes the average a fragile summary. For example, the same Gemini prompt-chaining configuration that scores 74.34% on LibBit scores 0% on LibRLP, LibZip, Multicallable, and ERC1967FactoryConstants, and N/E on many other contracts. The abstract's 'closely approaching' language is only justified for individual contracts such as LibBit, not for the average. The paper should add a paired or per-contract analysis, and the conclusion should be explicitly limited to the per-contract existence result unless the average can be recomputed fairly.
minor comments (5)
  1. [Section III-C; Section III-D] The mutation score definition is inconsistent: Section III-C defines the denominator as non-equivalent mutants, while Section III-D uses 'Total Number of Mutants'. Please align the formulas and state how Sumo handles equivalent mutants.
  2. [Section II-C; Section III-A] The paper motivates best-of-five selection by LLM nondeterminism but reports temperature=0 for all models. Please clarify whether the five requests were all made at temperature=0 and, if so, whether the observed variance is due to API nondeterminism.
  3. [Section II-C; Section III-B] In the few-shot condition, the retrieved examples include Solady's human-written test properties, and the same Solady tests are used as the human benchmark. This should be acknowledged as a potential contamination or independence limitation, especially since the few-shot condition performs worst.
  4. [Table II; Section IV] The table would benefit from a column that reports the number of contracts included in each average, and the caption should explicitly define N/A (not available) versus N/E (non-executable) and state how each is treated in the average row.
  5. [Throughout] There is no artifact link or replication package. Given the complexity of the pipeline (LLM APIs, Foundry, Sumo, manual repair, best-of-five selection), a public artifact with per-request data and repair logs would materially improve verifiability.

Circularity Check

0 steps flagged · score 2.0 of 10

No construction-level circularity; mutation scores are external measurements. One minor non-load-bearing self-citation does not force the central claim.

full rationale

The central result is an externally measured mutation score (killed mutants divided by non-equivalent mutants) computed by Sumo/Foundry on LLM-generated properties, compared with the same metric on Solady's human-written tests. No fitted parameter, hidden equation, or definitional identity links the prompt-chaining output to the human benchmark: prompt chaining (Section II-C, Listings 3-4) uses only the contract source and natural-language functionality descriptions, not the human-written test properties. The few-shot condition does place Solady's human-written tests in the prompt (Section II-C: 'Each example includes a smart contract and its corresponding test properties'), but the target contract's own tests are excluded and the few-shot scores are the lowest, so no favorable result is forced by construction. The paper's sole self-citation, [17] (M. Hassan et al., sharing author M. Hassan with this paper), is invoked only as 'inspiration' for listing English properties before converting to Solidity; it is not used to justify the measured mutation scores. The exclusion of non-executable outputs ('we select only those test properties from the generated set that are executable or can be made executable with minimal manual effort'; Table II marks N/E cells) and the best-of-five selection are genuine measurement/validity concerns about whether 25.99% is an unbiased LLM-capability estimate, but they do not make the derivation equivalent to its inputs. Under the stated rubric, no load-bearing step reduces to its own inputs.

Assumptions & free parameters 2 free parameters · 5 assumptions · 0 invented entities

The central claim rests on the measurement pipeline (mutation testing, best-of-five selection, manual repair, human baseline) rather than on fitted constants or new entities. The main burden is that the reported average depends on subjective and selective decisions that are not quantified.

free parameters (2)
  • Number of LLM generation attempts (best-of-N selection) = up to 5, selected output with most executable properties
    Hand-chosen; selecting the best of multiple calls raises executable-property rates and mutation scores relative to a single sample, and the paper does not report single-call expectations.
  • Few-shot retrieval neighbor count k = 2
    Hand-chosen KNN setting; without a similarity threshold, irrelevant examples can be retrieved, which the authors themselves suggest explains the low few-shot mutation scores.
assumptions (5)
  • domain assumption Mutation score is a valid proxy for test-property quality.
    The entire evaluation uses Sumo mutation scores to rank property quality; no manual review of the bugs caught by LLM properties is reported.
  • domain assumption The Solady human-written test properties are an appropriate expert baseline.
    These are the reference tests used both for few-shot examples and the 31.75% benchmark; their representativeness as expert tests is taken as given.
  • ad hoc to paper Outputs that the authors manually repaired are still attributable to the LLM.
    Section III-F describes manually fixing compilation errors and including those properties in mutation testing; no audit of the amount or effect of repair is provided.
  • domain assumption Sumo's mutant set is composed of non-equivalent mutants as claimed.
    The mutation score formula uses 'non-equivalent mutants' but the paper never describes equivalent-mutant detection.
  • ad hoc to paper Best-of-five output selection is a fair representation of LLM capability.
    Section II-C chooses the output with more executable properties out of up to five generations; this is a selection rule, not a random sample.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Towards LLM-assisted High-Quality Property Generation for Solidity Smart Contracts." pith.science (2026). https://pith.science/paper/V5YL2Y2U

@misc{pith2026260723308,
  author       = {Pith},
  title        = {Pith review of: Towards LLM-assisted High-Quality Property Generation for Solidity Smart Contracts},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/V5YL2Y2U}},
  note         = {Machine review of arXiv:2607.23308}
}
read the original abstract

The immutable nature of smart contracts makes it challenging to fix and patch bugs once they are deployed to a blockchain. This implies that security vulnerabilities may be exposed to possible exploitation for a longer period, necessitating comprehensive pre-deployment testing. Property-based testing combined with fuzzing has proven itself as a promising technique for uncovering vulnerabilities. Traditionally, system properties are written by human experts, which is time-consuming and consequently expensive.With the recent advancement in Large Language Models (LLMs) and their ability to 'understand' natural language and code semantics, it may be possible to generate effective properties. This study, leverages state-of-the-art LLMs to generate high-quality properties for Soliditybased smart contracts. We measure the quality of the generated properties using mutation testing. Our results show that LLMs have the potential to generate high-quality properties that are close to those written by human experts. We extensively evaluate LLMs using various prompting techniques (e.g., zero shot, few shot, and prompt chaining). Overall, we find that Gemini Pro 1.5, when combined with prompt chaining, achieves the highest average mutation score of 25.99% among all studied configurations, closely approaching the human written benchmark of 31.75%. However, our per contract analysis reveals notable variance, particularly for the LibBit contract, where Gemini Pro 1.5 under prompt chaining achieves a mutation score of 74.34%, which is on par with human written properties (74.83%). This highlights that while average performance is informative, individual contract level results demonstrate that LLMs can, in some cases, match expert level property generation.

Figures

Figures reproduced from arXiv: 2607.23308 by the authors.

Figure 1
Figure 1. First, in the input loading phase, we take all [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 1
Figure 1. A high-level workflow of the LLM-assisted approach for generating high-quality properties for Solidity [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Bar charts (a) - (c) show the effectiveness of prompting techniques for generating properties on LLMs [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

44 extracted references · 6 linked inside Pith

  1. [1]

    Soltype: Refinement types for arithmetic overflow in solidity,

    B. Tan, B. Mariano, S. K. Lahiri, I. Dillig, and Y . Feng, “Soltype: Refinement types for arithmetic overflow in solidity,”Proceedings of the ACM on Programming Languages, vol. 6, no. POPL, pp. 1–29, 2022

    2022

  2. [2]

    Sereum: Protecting existing smart con- tracts against re-entrancy attacks,

    M. Rodler, W. Li, G. O. Karame, and L. Davi, “Sereum: Protecting existing smart con- tracts against re-entrancy attacks,”arXiv preprint arXiv:1812.05934, 2018

    arXiv 2018

  3. [3]

    Cross-contract static analysis for detect- ing practical reentrancy vulnerabilities in smart contracts,

    Y . Xue, M. Ma, Y . Lin, Y . Sui, J. Ye, and T. Peng, “Cross-contract static analysis for detect- ing practical reentrancy vulnerabilities in smart contracts,” inProceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, 2020, pp. 1029–1040

    2020

  4. [4]

    The dao attacked: Code issue leads to $60 million ether theft,

    M. del Castillo, “The dao attacked: Code issue leads to $60 million ether theft,”CoinDesk, 2016, Accessed: 2024-07-31. [Online]. Available: https: //www.coindesk.com/markets/2016/06/17/the- dao - attacked - code - issue - leads - to - 60- million - ether-theft/

    2016

  5. [5]

    Property-based testing in practice,

    H. Goldstein, J. W. Cutler, D. Dickstein, B. C. Pierce, and A. Head, “Property-based testing in practice,” inProceedings of the IEEE/ACM 46th International Conference on Software Engineer- ing, 2024, pp. 1–13

    2024

  6. [6]

    Propertygpt: Llm-driven formal verification of smart contracts through retrieval- augmented property generation,

    Y . Liu et al., “Propertygpt: Llm-driven formal verification of smart contracts through retrieval- augmented property generation,”arXiv preprint arXiv:2405.02580, 2024

    arXiv 2024

  7. [7]

    Can large language models write good property-based tests?

    V . Vikram, C. Lemieux, and R. Padhye, “Can large language models write good property-based tests?”arXiv preprint arXiv:2307.04346, 2023

    arXiv 2023

  8. [8]

    Retrieval-based prompt selection for code-related few-shot learning,

    N. Nashid, M. Sintaha, and A. Mesbah, “Retrieval-based prompt selection for code-related few-shot learning,” in2023 IEEE/ACM 45th In- ternational Conference on Software Engineering (ICSE), IEEE, 2023, pp. 2450–2462. 12

    2023

Show all 44 references
  1. [9]

    com / Vectorized / solady / commit / 58362f785c90c6693e44f358fac594b0851bb357, 2024

    Vectorized,Solady: Optimized solidity snippets, https : / / github. com / Vectorized / solady / commit / 58362f785c90c6693e44f358fac594b0851bb357, 2024

    2024

  2. [10]

    [On- line]

    npm-stat,Solady download statistics, 2025. [On- line]. Available: https://npm-stat.com/charts.html? package=solady

    2025

  3. [11]

    Foundry,Foundry: A blazing fast, portable and modular toolkit for ethereum application develop- ment written in rust, https://github.com/foundry- rs/foundry, Accessed: 2024-07-30, 2023

    2024

  4. [12]

    A systematic review of fuzzing,

    X. Zhao, H. Qu, J. Xu, X. Li, W. Lv, and G.-G. Wang, “A systematic review of fuzzing,”Soft Computing, vol. 28, no. 6, pp. 5493–5522, 2024

    2024

  5. [13]

    Barboni,Sumo: Mutation testing tool for solidity smart contracts, https : / / github

    M. Barboni,Sumo: Mutation testing tool for solidity smart contracts, https : / / github . com / MorenaBarboni/SuMo-SOlidity-MUtator, GitHub repository, 2024

    2024

  6. [14]

    [Online]

    Foundry,Foundry: A fast, portable and modu- lar toolkit for ethereum application development, GitHub Repository, 2023. [Online]. Available: https://github.com/foundry-rs/foundry [15]Prompt engineering guide: Zero-shot prompt, https : / / www . promptingguide . ai / techniques ...

    2023

  7. [17]

    Llm-guided formal veri- fication coupled with mutation testing,

    M. Hassan, S. Ahmadi-Pour, K. Qayyum, C. K. Jha, and R. Drechsler, “Llm-guided formal veri- fication coupled with mutation testing,” in2024 Design, Automation & Test in Europe Conference & Exhibition (DATE), IEEE, 2024, pp. 1–2. [18]Prompt engineering guide: Few-shot prompting...

    2024

  8. [20]

    emanuelecivini

    GasBad,Gasbad - comparing gas efficiency of solidity libraries, https : / / www. emanuelecivini . com/post/gas-bad/, Accessed: 2025-05-02, 2023

    2025

  9. [21]

    xyz / crowdfund / solady, Accessed: 2025-05-02, 2025

    Cantina,Solady security review, https://cantina. xyz / crowdfund / solady, Accessed: 2025-05-02, 2025

    2025

  10. [22]

    Smart contract: Attacks and protections,

    S. Sayeed, H. Marco-Gisbert, and T. Caira, “Smart contract: Attacks and protections,”Ieee Access, vol. 8, pp. 24 416–24 427, 2020

    2020

  11. [23]

    A survey of ethereum smart contract se- curity: Attacks and detection,

    T. Jiao, Z. Xu, M. Qi, S. Wen, Y . Xiang, and G. Nan, “A survey of ethereum smart contract se- curity: Attacks and detection,”Distributed Ledger Technologies: Research and Practice,

  12. [24]

    Smart contract vulnerability analysis and security audit,

    D. He, Z. Deng, Y . Zhang, S. Chan, Y . Cheng, and N. Guizani, “Smart contract vulnerability analysis and security audit,”IEEE Network, vol. 34, no. 5, pp. 276–282, 2020

    2020

  13. [25]

    Gptscan: Detecting logic vul- nerabilities in smart contracts by combining gpt with program analysis,

    Y . Sun et al., “Gptscan: Detecting logic vul- nerabilities in smart contracts by combining gpt with program analysis,” inProceedings of the IEEE/ACM 46th International Conference on Soft- ware Engineering, 2024, pp. 1–13

    2024

  14. [26]

    Finding permission bugs in smart contracts with role min- ing,

    Y . Liu, Y . Li, S.-W. Lin, and C. Artho, “Finding permission bugs in smart contracts with role min- ing,” inProceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, 2022, pp. 716–727

    2022

  15. [27]

    Slither: A static analysis framework for smart contracts,

    J. Feist, G. Grieco, and A. Groce, “Slither: A static analysis framework for smart contracts,” in2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB), IEEE, 2019, pp. 8–15

    2019

  16. [28]

    Madmax: Surviv- ing out-of-gas conditions in ethereum smart con- tracts,

    N. Grech, M. Kong, A. Jurisevic, L. Brent, B. Scholz, and Y . Smaragdakis, “Madmax: Surviv- ing out-of-gas conditions in ethereum smart con- tracts,”Proceedings of the ACM on Programming Languages, vol. 2, no. OOPSLA, pp. 1–27, 2018

    2018

  17. [29]

    Smartcheck: Static analysis of ethereum smart contracts,

    S. Tikhomirov, E. V oskresenskaya, I. Ivanitskiy, R. Takhaviev, E. Marchenko, and Y . Alexandrov, “Smartcheck: Static analysis of ethereum smart contracts,” inProceedings of the 1st international workshop on emerging trends in software engi- neering for blockchain, 2018, pp. 9–16

    2018

  18. [30]

    Manticore: A user-friendly symbolic execution framework for binaries and smart contracts,

    M. Mossberg et al., “Manticore: A user-friendly symbolic execution framework for binaries and smart contracts,” in2019 34th IEEE/ACM In- ternational Conference on Automated Software Engineering (ASE), IEEE, 2019, pp. 1186–1189

    2019

  19. [31]

    Team,Mythril: Security analysis tool for ethereum smart contracts, 2018

    C. Team,Mythril: Security analysis tool for ethereum smart contracts, 2018

    2018

  20. [32]

    Making smart contracts smarter,

    L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor, “Making smart contracts smarter,” in Proceedings of the 2016 ACM SIGSAC conference on computer and communications security, 2016, pp. 254–269

    2016

  21. [33]

    Formal verification of smart contracts: Short paper,

    K. Bhargavan et al., “Formal verification of smart contracts: Short paper,” inProceedings of the 2016 ACM workshop on programming languages and analysis for security, 2016, pp. 91–96

    2016

  22. [34]

    Zeus: Analyzing safety of smart contracts,

    S. Goel, M. Dhawan, S. Sharma, and S. Kalra, “Zeus: Analyzing safety of smart contracts,” 2018

    2018

  23. [35]

    Finding software vulnerabilities by smart fuzzing,

    S. Bekrar, C. Bekrar, R. Groz, and L. Mounier, “Finding software vulnerabilities by smart fuzzing,” in2011 Fourth IEEE International Conference on Software Testing, Verification and Validation, IEEE, 2011, pp. 427–430

    2011

  24. [36]

    Fuzzing: A survey,

    J. Li, B. Zhao, and C. Zhang, “Fuzzing: A survey,” Cybersecurity, vol. 1, p. 6, 2018.DOI: 10.1186/ s42400 - 018 - 0002 - y [Online]. Available: https : //doi.org/10.1186/s42400-018-0002-y 13

    2018 doi

  25. [37]

    Fuzzing: State of the art,

    H. Liang, X. Pei, X. Jia, W. Shen, and J. Zhang, “Fuzzing: State of the art,”IEEE Transactions on Reliability, vol. 67, no. 3, pp. 1199–1218, 2018

    2018

  26. [38]

    Contract- fuzzer: Fuzzing smart contracts for vulnerability detection,

    B. Jiang, Y . Liu, and W. K. Chan, “Contract- fuzzer: Fuzzing smart contracts for vulnerability detection,” inProceedings of the 33rd ACM/IEEE international conference on automated software engineering, 2018, pp. 259–269

    2018

  27. [39]

    [Online]

    Cyclic,Echidna: Ethereum smart contract fuzzer, GitHub Repository, 2023. [Online]. Available: https://github.com/crytic/echidna

    2023

  28. [40]

    Formal specification and verifi- cation of smart contracts for azure blockchain,

    Y . Wang et al., “Formal specification and verifi- cation of smart contracts for azure blockchain,” arXiv preprint arXiv:1812.08829, 2018

    2018 arXiv

  29. [41]

    Invcon: A dynamic invari- ant detector for ethereum smart contracts,

    Y . Liu and Y . Li, “Invcon: A dynamic invari- ant detector for ethereum smart contracts,” in Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering, 2022, pp. 1–4

    2022

  30. [42]

    Automated invariant generation for solidity smart contracts,

    Y . Liu, C. Zhang, et al., “Automated invariant generation for solidity smart contracts,”arXiv preprint arXiv:2401.00650, 2024

    2024 arXiv

  31. [43]

    Large language models are zero-shot fuzzers: Fuzzing deep-learning libraries via large language models,

    Y . Deng, C. S. Xia, H. Peng, C. Yang, and L. Zhang, “Large language models are zero-shot fuzzers: Fuzzing deep-learning libraries via large language models,” inProceedings of the 32nd ACM SIGSOFT international symposium on soft- ware testing and analysis, 2023, pp. 423–435

    2023

  32. [44]

    Large language models are edge- case generators: Crafting unusual programs for fuzzing deep learning libraries,

    Y . Deng, C. S. Xia, C. Yang, S. D. Zhang, S. Yang, and L. Zhang, “Large language models are edge- case generators: Crafting unusual programs for fuzzing deep learning libraries,” inProceedings of the 46th IEEE/ACM International Conference on Software Engineering, 2024, pp. 1–13

    2024

  33. [45]

    Smartinv: Multimodal learning for smart contract invariant inference,

    S. J. Wang, K. Pei, and J. Yang, “Smartinv: Multimodal learning for smart contract invariant inference,” in2024 IEEE Symposium on Security and Privacy (SP), IEEE Computer Society, 2024, pp. 126–126

    2024

  34. [46]

    LASP: LLM Assisted Secu- rity Property Generation for SoC Verification,

    A. Ayalasomayajula, R. Guo, J. Zhou, S. K. Saha, and F. Farahmandi, “LASP: LLM Assisted Secu- rity Property Generation for SoC Verification,” in Proceedings of the 2024 ACM/IEEE International Symposium on Machine Learning for CAD (ML- CAD), 2024, pp. 1–7

    2024

  35. [47]

    LLM-based Property-based Test Generation for Guardrail- ing Cyber-Physical Systems,

    K. Etemadi, M. Sirjani, M. H. Moghadam, P. Strandberg, and P. Pettersson, “LLM-based Property-based Test Generation for Guardrail- ing Cyber-Physical Systems,”arXiv preprint arXiv:2505.23549, 2025

    2025 arXiv

  36. [48]

    Learning contract invariants using reinforcement learning,

    J. Liu, Y . Chen, B. Tan, I. Dillig, and Y . Feng, “Learning contract invariants using reinforcement learning,” inProceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering, 2022, pp. 1–11. 14

    2022

Pith tools

Reviewed July 31, 2026 · model on record in the stance chip above.