Pith. sign in

REVIEW 4 major objections 6 minor 91 references

SmartInv: Multimodal Learning for Smart Contract Invariant Inference

T0 review · 4 major / 6 minor · reviewed 2026-08-12 · deepseek-v4-flash

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

Pith's one-line read SmartInv claims that finetuning a foundation model to reason across source code and natural-language documentation can generate verifier-checked invariants that reveal functional smart contract bugs missed by pattern-based analyzers.

desk verdict SmartInv is a genuinely useful system with a credible refined evaluation, but the headline bug counts outrun the evidence until the confirmation protocol and zero-day list are published. read the letter →

arxiv 2411.09217 v1 pith:P7ND2CZR submitted 2024-11-14 cs.SE cs.CRcs.PL

Sally Junsong Wang , Kexin Pei , Junfeng Yang This is my paper · ORCID
classification cs.SEcs.CRcs.PL
keywords smartcontractsecurityinvariantinferencefunctionalbugsfoundationmodelsmultimodalreasoningTierofThoughtformalverificationSolidity
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

SmartInv tries to establish that the functional bugs which escape pattern-based analyzers can be found automatically by treating source code and natural-language documentation as two modalities and asking a finetuned foundation model to generate invariants from both. The paper's claim is that expected behavior, expressed as invariant assertions, is the bridge that lets a verifier turn model guesses into confirmed bugs. It reports that on 89,621 real-world contracts the method produces 3.5x more bug-critical invariants and finds 4x more critical bugs than previous tools, in roughly 150x less time, and that it uncovered 119 previously unknown vulnerabilities, five confirmed as high severity. A reader should care because price-manipulation and privilege-escalation bugs, which account for a large share of exploit losses, currently require human auditors to reason across context that source code alone does not contain.

What carries the argument

The load-bearing mechanism is Tier of Thought (ToT), a three-tier prompting and finetuning procedure that decomposes invariant inference into progressively harder questions: transactional context and critical program points, then invariants and bug-preventive invariants, then ranking and vulnerability prediction. The invariants themselves are drawn from smart-contract-specific templates, including assertions at program points, entry-state comparisons like $\mathrm{Old}(\mathit{expr})$ with a volatility ratio $k$ (default 2), mapping-wide sums via $\mathrm{SumMapping}(\cdot)$, function modifiers, and cross-function properties. ToT's ranked output feeds a verification loop that first tries an inductive correctness proof and, failing that, asks a bounded model checker for counterexamples; a counterexample is either a confirmed bug or evidence that the model's invariant was wrong. This combination is what lets ungrounded model guesses be filtered by sound checking before they appear in a report.

What would settle it

Hold out a set of contracts and strip or contradict their comments, then run SmartInv: if true-positive bug detection falls to the level of code-only tools or false-positive invariants jump sharply, the claimed multimodal gain is a comment-quality effect, not a general reasoning ability.

Watch

Extended reading notes

Core claim

The paper's central claim is that invariant inference for smart contracts is a multimodal reasoning task: the code defines how state changes, while comments and documentation define how state is supposed to change, and neither alone is enough for functional bugs. SmartInv finetunes a foundation model with a staged prompting scheme (Tier of Thought) that first predicts transactional context and critical program points, then generates invariants at those points, then ranks them, and finally verifies each ranked invariant with induction and bounded model checking. Verified invariants that are violated become bug reports, and violations that cannot be proven are inspected to separate true bugs from incorrect invariants. On the paper's evaluation, this pipeline rediscovers bugs behind multi-million-dollar exploits and detects previously unknown functional bugs that symbolic-execution and static-analysis tools miss.

Load-bearing premise

The pipeline assumes the natural-language comments and documentation in the contract source describe the behavior the contract is supposed to have; if comments are missing, stale, or misleading, the generated invariants lose their ground truth.

Editorial extensions

If this is right

  • Functional bugs whose detection requires reading comments and transaction context become checkable before deployment, rather than only after a hack.
  • Verifier-backed invariant checking turns model suggestions into provable properties, so hallucinated invariants are weeded out before they reach a report.
  • The same tiered prompting recipe can be applied to other domains where expected behavior is written in natural-language prose rather than code alone.
  • Detecting price-manipulation and privilege-escalation bugs at source level means audits can scale to hundreds of thousands of contracts in minutes per contract.

Reading between the lines

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

  • If comments are absent, stale, or adversarial, every downstream invariant and bug report loses its ground truth; the paper's reported gains are best read as applying to contracts whose prose matches behavior.
  • A testable extension is to measure SmartInv on contracts with intentionally misleading comments to quantify how much of the 4x gain is natural-language signal versus code-only pattern learning.
  • Since adding transaction history as a modality improved precision and F1, for already-deployed contracts including on-chain execution traces should further reduce false positives.
  • The approach likely transfers to other languages with strong natural-language specifications, but the invariant templates ($\mathrm{Old}$, $k$-ratio, $\mathrm{SumMapping}$) are Solidity-specific and would need re-engineering.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 6 minor

Summary. The paper presents SmartInv, a framework that fine-tunes LLaMA-7B with a tiered prompting strategy (Tier of Thought, ToT) to infer smart contract invariants from source code and natural-language comments, then uses Boogie/CORRAL-based verification (built on VeriSol) to prove or falsify the inferred invariants and report counterexamples as potential bugs. The central claim is that SmartInv detects functional, 'machine un-auditable' bugs that prior automated tools miss, supported by headline numbers: 51,505 counterexamples converted to 46,360 confirmed bugs, 119 zero-day vulnerabilities (five developer-confirmed critical), a 3.5x improvement in bug-critical invariants, a 4x improvement in critical bug detection, and a 150x speedup over state-of-the-art tools. The evaluation includes a large-scale run on 89,621 contracts, a refined experiment on 1,241 contracts from 60 hacked projects with audit reports, an ablation study isolating the contribution of natural language, ToT, labeled features, and model optimization, and runtime comparisons.

Significance. If the central claims hold, SmartInv is a valuable step forward: it demonstrates a workable pipeline for turning LLM-generated invariants into verifier-checked bug reports, and the refined experiment on 60 hacked projects with audit-report ground truth is the strongest evidence in the paper and supports the qualitative claim that SmartInv finds functional bugs that other tools miss. The ToT prompting strategy, the release of the dataset and tool, the ablation isolating the effect of natural-language modality (F1 drops from 0.82 to 0.45 without comments), and the reported 150x runtime advantage over symbolic-execution tools are concrete contributions. However, the headline quantitative claims (46,360 confirmed bugs, 119 zero-days, 5 developer-confirmed critical bugs) rest on an undocumented conversion from verifier counterexamples to ground-truth bugs, and the paper's own limitations section concedes that exploitability was not assessed. The paper's significance is therefore conditional on the availability of an audit trail for those numbers; as written, the contribution is solid but the headline is over-claimed.

major comments (4)
  1. [§3.4 and Table 6] The conversion of 51,505 counterexamples into 46,360 'confirmed bugs' is load-bearing for the abstract's claims, but no confirmation protocol is provided. The Boogie/CORRAL verifier can only show that the contract violates the model-supplied invariant; it cannot show that the invariant is the intended specification. The caption of Table 6 further states that SmartInv's reported results include both verifier-produced bugs and LLM-reported bugs, which conflates verified counterexamples with unverified model predictions. Please provide itemized per-contract data, the confirmation criteria, inter-rater reliability, and a list of the claimed zero-day bugs, or restrict the headline claims to the refined audit-report-based experiment.
  2. [§2.2, Table 3, and §3.2] The invariant assert(price <= Old(price)*k) with default k=2 encodes an unstated assumption that any price change beyond a factor of 2 is a bug. This is a free parameter, not a specification extracted from the contract or from domain documentation. Because this invariant template drives the price-manipulation and inconsistent-state bug counts, the 90.01% 'confirmed bug' rate is not meaningful without a sensitivity analysis over k and without evidence that k=2 matches developer intent. Please report how the counts vary with k, and distinguish contracts that contain explicit volatility bounds from those where the bound is entirely invented by the model.
  3. [Algorithm 1, line 14] The pseudocode breaks out of the while loop immediately after the first counterexample is found (line 14: 'break; // manual inspection requested for counterexamples'). As written, this means at most one candidate invariant per contract is ever processed through the bounded-model-checking phase, which is inconsistent with Table 6's per-contract multi-bug counts and with the reported 51,505 counterexamples. If the intended behavior is to pause for inspection and then continue with the remaining invariants, the algorithm is wrong as printed; if it truly stops, the verification coverage and the counterexample totals need to be re-derived.
  4. [§7 and §6] The paper claims 119 zero-day vulnerabilities, five confirmed by developers as 'high severity,' and a $17,600 bounty, but provides only two anonymized examples and no developer-communication evidence, no itemized list, and no exploitability assessment. Section 6 explicitly states that 'we did not report results based on bugs' exploitability' and that manual classification 'can be subjective in some cases.' The 'critical zero-day' claim therefore overstates what the evaluation supports; either supply the full confirmation trail or downgrade the claim to 'reported potential vulnerabilities awaiting developer confirmation.'
minor comments (6)
  1. [§1] The Introduction contains a typo: 'annd hopefully' should be 'and hopefully.'
  2. [§2.2] The phrase 'National Commmon Vulnerabilities and Exposures (CVE)' contains a typo: 'Commmon' should be 'Common.'
  3. [§5.2] The word 'langauges' in the INVCON discussion should be 'languages.'
  4. [§6] The section ends with the header 'Ethical Disclosure.' followed by no text; either add the ethical disclosure or remove the placeholder.
  5. [§5.3] In the 'Effect of Quantization and PEFT' paragraph, the text says both models 'had the same F1 score of 94%,' but Table 11 lists F1 = 0.82 for both; the 94% appears to be an error.
  6. [Table 8] The refined experiment table is very difficult to read: several rows contain more entries than the column structure allows, and the totals row is not legibly formatted. Please provide a machine-readable version or a clearer layout, since this table is central to the false-positive/false-negative claims.

Circularity Check

2 steps flagged · score 6.0 of 10

Headline bug counts are defined by the tool's own invariants and verifier; training labels come from the same verification pipeline.

  1. self definitional [Section 2.2, Table 3 (price manipulation example)]
    "k is an adjustable ratio, where SMART INV sets default as k=2. Any violation of the assertion invariant would signal price volatility exceeding user desired k and thus would signal price manipulation."

    The 'price manipulation' bug is defined as a violation of assert(price <= Old(price)*k) with k=2 chosen by the authors. The code and comments in Listing 2 do not state any 2x volatility bound; the bound is an input assumption, not a derived property. Therefore a reported PM bug is, by construction, the negation of the tool's own assertion. Table 6's PM=2,651 count is a count of violations of this author-set threshold, so the predicted vulnerability reduces to the logical complement of the input invariant. The Visor exploit is externally confirmed, but the general detection claim is definitional.

  2. fitted input called prediction [Section 4 (Labeled Features) and Section 3.4 (ToT Invariants Verification Algorithm)]
    "To ensure correct critical program points and invariant labels, we ran the verification algorithm in §3.4 and cross-checking with at least two researchers. ... During verification, SMART INV produced 51,505 counterexamples on 89,621 real-world contracts. Upon review, 46,360 (90.01%) counterexamples resulted from confirmed bugs and 5,145 (9.99%) counterexamples were due to incorrectly inferred invariants."

    The training-time notion of a 'correct critical invariant' is fixed by the exact Algorithm 1 (§3.4) that later produces counterexamples at inference: inductive checking plus CORRAL bounded model checking. The model is finetuned to emit invariants that this same algorithm judges to be bug-preventive, and then the same algorithm's counterexamples are counted as discovered bugs (51,505) and, after manual review, 46,360 'confirmed bugs.' The training signal and the large-scale evaluation signal are thus the same machinery; the headline bug counts are a self-consistency check of the training/evaluation loop rather than an independent measurement.

full rationale

The paper's strongest claims are the abstract's 119 zero-day vulnerabilities, the 4x critical-bug improvement, and the 46,360 'confirmed bugs' from 51,505 counterexamples. Two load-bearing reductions make these counts partially definitional. First, price manipulation is operationally defined as any violation of assert(price <= Old(price)*k) with a default k=2; no external spec in the motivating example states that bound, so the predicted bug is the logical complement of the tool's own chosen assertion. Counting PM bugs is counting violations of that assertion. Second, the 'critical invariant' labels used to finetune the model were generated by running the same §3.4 verification algorithm that later produces the counterexample-based bug reports. The model is trained to replicate that algorithm's judgments, and the same algorithm's counterexamples are then reported as discovered bugs, making the large-scale evaluation self-referential. This is not a dismissal of the refined experiments, which use audit reports as ground truth and show genuine independent gains, nor of the two developer-confirmed zero-day case studies; those give the paper real external content and keep the finding at partial rather than total circularity. But the headline numbers rest on invariant definitions and a verification pipeline internal to the paper, so the central claim partially reduces to its own inputs.

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

The central claim rests mainly on domain assumptions rather than free parameters. The only explicit numeric knob that directly changes detection results is k=2 in the price invariant. The largest burden is treating source-code comments as specifications and trusting that a counterexample to a model-generated invariant is a bug after a lightly described manual review. No new physical entities are introduced; the custom assertion constructs (Old, SumMapping, Invariant) are software artifacts, not postulated entities.

free parameters (1)
  • price volatility ratio k = 2 (default)
    Table 3 and Section 3.2: the invariant assert(price <= Old(price)*k) defines what counts as price manipulation, and k=2 is chosen by the authors. This hand-set threshold directly determines the bug-detection criteria, and no principled derivation or sensitivity analysis is given.
assumptions (4)
  • domain assumption Natural-language comments and documentation in smart contract source accurately describe intended behavior
    SMART-INV treats NL comments as ground truth for expected behavior (e.g., price should stay within range) and uses them to train and validate invariants. Stale, missing, or misleading comments would make inferred invariants wrong. Invoked in Section 2.1, Section 3.2, and the Listing 1-3 examples.
  • domain assumption Most blockchain users are honest, so Old(price) captures a non-manipulated baseline
    Section 2.2 argues an attacker cannot easily manipulate the pre-transaction price because most users are honest. The price-manipulation invariant depends on this empirical claim, which is asserted without quantitative evidence.
  • domain assumption A counterexample to a generated invariant indicates a bug rather than an incorrect invariant after manual review
    Section 3.4 says counterexamples have two readings; the paper assigns 90.01% of them to bugs after a review process that is not described. This assumption is load-bearing for the 51,505 reported bugs.
  • domain assumption VeriSol and Boogie's Solidity-to-Boogie translation is semantically faithful for supported compiler versions
    The inductive proof and bounded model checking phases depend on VeriSol's translation (Section 3.4), and Section 6 acknowledges it only works for Solidity 0.4.0 to 0.7.0. For other compiler versions the paper falls back to manual review, which is not a verified procedure.

how reviews work

0 comments
Cite this review

Pith. "Pith review of SmartInv: Multimodal Learning for Smart Contract Invariant Inference." pith.science (2026). https://pith.science/paper/P7ND2CZR

@misc{pith2026241109217,
  author       = {Pith},
  title        = {Pith review of: SmartInv: Multimodal Learning for Smart Contract Invariant Inference},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/P7ND2CZR}},
  note         = {Machine review of arXiv:2411.09217}
}
abstract

Smart contracts are software programs that enable diverse business activities on the blockchain. Recent research has identified new classes of "machine un-auditable" bugs that arise from both transactional contexts and source code. Existing detection methods require human understanding of underlying transaction logic and manual reasoning across different sources of context (i.e. modalities), such as code, dynamic transaction executions, and natural language specifying the expected transaction behavior. To automate the detection of ``machine un-auditable'' bugs, we present SmartInv, an accurate and fast smart contract invariant inference framework. Our key insight is that the expected behavior of smart contracts, as specified by invariants, relies on understanding and reasoning across multimodal information, such as source code and natural language. We propose a new prompting strategy to foundation models, Tier of Thought (ToT), to reason across multiple modalities of smart contracts and ultimately to generate invariants. By checking the violation of these generated invariants, SmartInv can identify potential vulnerabilities. We evaluate SmartInv on real-world contracts and re-discover bugs that resulted in multi-million dollar losses over the past 2.5 years (from January 1, 2021 to May 31, 2023). Our extensive evaluation shows that SmartInv generates (3.5X) more bug-critical invariants and detects (4$\times$) more critical bugs compared to the state-of-the-art tools in significantly (150X) less time. \sys uncovers 119 zero-day vulnerabilities from the 89,621 real-world contracts. Among them, five are critical zero-day bugs confirmed by developers as ``high severity.''

Figures

Figures reproduced from arXiv: 2411.09217 by the authors.

Figure 1
Figure 1. SMARTINV’s Workflow multimodal information that also respects smart contract semantics during finetuning. Our evaluation shows that sim￾ply prompt engineering without customized training datasets cannot identify correct invariants in real-world contracts. To overcome the challenge, we have designed tailored invariant templates (in §3.2) and built a unique finetuning process (in §3.1) that incorporates multimodal inf… view at source ↗
Figure 2
Figure 2. Comparison of SMARTINV with three prompting￾based tools using the 1,241 contracts in the refined experi￾ments of [PITH_FULL_IMAGE:figures/full_fig_p011_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

91 extracted references · 69 canonical work pages

  1. [1]

    Crytic safety properties: https://github.com/crytic/properties

  2. [2]

    Etherscan: https://etherscan.io/

  3. [3]

    Gemma strategies: https://github.com/gammastrategies/uniswapv3- risk-mitigation/blob/main/notes%20on%20uniswap%20v3 %20risk%20mitigation.md

  4. [4]

    Smart contract security field guide: https://scsfg.io/hackers/oracle- manipulation/

  5. [5]

    Visor attack address: 0x10c509aa9ab291c76c45414e7cdbd375e1d5ace8

  6. [6]

    SMT-based verification of solidity smart contracts

    Leonardo Alt and Christian Reitwiessner. SMT-based verification of solidity smart contracts. In Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, 2018

    2018

  7. [7]

    Eth2vec: learning contract-wide code representations for vulnerability detection on ethereum smart contracts

    Nami Ashizawa, Naoto Yanai, Jason Paul Cruz, and Shingo Okamura. Eth2vec: learning contract-wide code representations for vulnerability detection on ethereum smart contracts. In Proceedings of the 3rd ACM International Symposium on Blockchain and Secure Critical Infrastructure. BSCI’21, 2021

    2021

  8. [8]

    The use of likely invariants as feedback for fuzzers

    Davide Balzarotti. The use of likely invariants as feedback for fuzzers. In 30th USENIX Security Symposium. USENIX Security’21 , 2021

    2021

Show all 91 references
  1. [9]

    Two vulnerabilities in one function — the analysis of visor finance exploit

    BEOSIN. Two vulnerabilities in one function — the analysis of visor finance exploit. Medium: https://beosin.medium.com/two- vulnerabilities-in-one-function-the-analysis-of-visor-finance-exploit- a15735e2492, 2021

    2021

  2. [10]

    Sailfish: Vetting smart contract state- inconsistency bugs in seconds

    Priyanka Bose, Dipanjan Das, Yanju Chen, Yu Feng, Christopher Kruegel, and Giovanni Vigna. Sailfish: Vetting smart contract state- inconsistency bugs in seconds. In 2022 IEEE Symposium on Security and Privacy. IEEE, 2022

    2022

  3. [11]

    Ethainter: a smart contract security analyzer for composite vulnerabilities

    Lexi Brent, Neville Grech, Sifis Lagouvardos, Bernhard Scholz, and Yannis Smaragdakis. Ethainter: a smart contract security analyzer for composite vulnerabilities. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation , 2020

    2020

  4. [12]

    Rich: Automatically protecting against integer-based vulnerabilities

    David Brumley, Tzi-cker Chiueh, Robert Johnson, Huijia Lin, and Dawn Song. Rich: Automatically protecting against integer-based vulnerabilities. 2007

    2007

  5. [13]

    When chatgpt meets smart contract vulnerability detection: How far are we? arXiv preprint arXiv:2309.05520, 2023

    Chong Chen, Jianzhong Su, Jiachi Chen, Yanlin Wang, Tingting Bi, Yanli Wang, Xingwei Lin, Ting Chen, and Zibin Zheng. When chatgpt meets smart contract vulnerability detection: How far are we? arXiv preprint arXiv:2309.05520, 2023

    2023 arXiv

  6. [14]

    Decoupling knowledge from memorization: Retrieval-augmented prompt learning

    Xiang Chen, Lei Li, Ningyu Zhang, Xiaozhuan Liang, Shumin Deng, Chuanqi Tan, Fei Huang, Luo Si, and Huajun Chen. Decoupling knowledge from memorization: Retrieval-augmented prompt learning. Advances in Neural Information Processing Systems , 35, 2022

    2022

  7. [15]

    https://github.com/ConsenSys/mythril

    Consensys/mythril, 2022. https://github.com/ConsenSys/mythril

    2022

  8. [16]

    Do you still need a manual smart contract audit? arXiv preprint arXiv:2306.12338 , 2023

    Isaac David, Liyi Zhou, Kaihua Qin, Dawn Song, Lorenzo Cavallaro, and Arthur Gervais. Do you still need a manual smart contract audit? arXiv preprint arXiv:2306.12338 , 2023

    2023 arXiv

  9. [17]

    The daikon system for dynamic detection of likely invariants

    Michael D Ernst, Jeff H Perkins, Philip J Guo, Stephen McCamant, Carlos Pacheco, Matthew S Tschantz, and Chen Xiao. The daikon system for dynamic detection of likely invariants. Science of computer programming, 69(1-3), 2007. 16

    2007

  10. [18]

    Slither: a static analysis framework for smart contracts

    Josselin Feist, Gustavo Grieco, and Alex Groce. Slither: a static analysis framework for smart contracts. In 2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain. IEEE, 2019

    2019

  11. [19]

    Post-mortem for vvisr staking contract exploit and upcoming migration

    Visor Finance. Post-mortem for vvisr staking contract exploit and upcoming migration. Medium:https://medium.com/visorfinance/post- mortem-for-vvisr-staking-contract-exploit-and-upcoming-migration- 7920e1dee55a, 2021

    2021

  12. [20]

    Ethbmc: A bounded model checker for smart contracts

    Joel Frank, Cornelius Aschermann, and Thorsten Holz. Ethbmc: A bounded model checker for smart contracts. In Srdjan Capkun and Franziska Roesner . 29th USENIX Security Symposium, USENIX Security, 2020

    2020

  13. [21]

    Defi token visr plunges by 95 Crypto Brief- ing: https://cryptoslate.com/defi-token-visr-plunges-by-95-following-8- million-hack/, 2021

    Liam Frost. Defi token visr plunges by 95 Crypto Brief- ing: https://cryptoslate.com/defi-token-visr-plunges-by-95-following-8- million-hack/, 2021

    2021

  14. [22]

    How effective are smart contract analysis tools? evaluating smart contract static analysis tools using bug injection

    Asem Ghaleb and Karthik Pattabiraman. How effective are smart contract analysis tools? evaluating smart contract static analysis tools using bug injection. In Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis , 2020

    2020

  15. [23]

    A survey of quantization methods for efficient neural network inference

    Amir Gholami, Sehoon Kim, Zhen Dong, Zhewei Yao, Michael W Mahoney, and Kurt Keutzer. A survey of quantization methods for efficient neural network inference. arXiv preprint arXiv:2103.13630 , 2021

    2021 arXiv

  16. [24]

    Timelockcontroller vulnerability in openzeppelin contracts

    Github. Timelockcontroller vulnerability in openzeppelin contracts. March 2022

    2022

  17. [25]

    Better language models and their implications

    OpenAI GPT2. Better language models and their implications. March 2022

    2022

  18. [26]

    Echidna: effective, usable, and fast fuzzing for smart contracts

    Gustavo Grieco, Will Song, Artur Cygan, Josselin Feist, and Alex Groce. Echidna: effective, usable, and fast fuzzing for smart contracts. In Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis , 2020

    2020

  19. [27]

    Alex Groce, Josselin Feist, Gustavo Grieco, and Michael Colburn. What are the actual flaws in important smart contracts (and how can we find them)? In Financial Cryptography and Data Security: 24th International Conference, FC 2020, Kota Kinabalu, Malaysia, February 10–14, 202...

    2020

  20. [28]

    An insecurity study of ethereum smart contracts

    Bishwas C Gupta, Nitesh Kumar, Anand Handa, and Sandeep K Shukla. An insecurity study of ethereum smart contracts. In Security, Privacy, and Applied Cryptography Engineering: 10th International Conference, SPACE 2020, Kolkata, India, December 17–21, 2020, Proceedings 10. Sprin...

    2020

  21. [29]

    Visor finance hack proof of concept

    Mudit Gupta. Visor finance hack proof of concept. Github link: https://gist.github.com/maxsam4/91704944a5d7b5923649ba7752f18f1a, 2021

    2021

  22. [30]

    10 real world use cases for ethereum

    Srajan Gupta. 10 real world use cases for ethereum. 2021

    2021

  23. [31]

    Discovering invariants via machine learning

    Seungwoong Ha and Hawoong Jeong. Discovering invariants via machine learning. Physical Review Research, 3(4)

  24. [32]

    solc-verify: A modular verifier for solidity smart contracts

    ´Akos Hajdu and Dejan Jovanovi ´c. solc-verify: A modular verifier for solidity smart contracts. In Verified Software. Theories, Tools, and Experiments: 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13–14, 2019, Revised Selected Papers 11 , page 1. Sp...

    2019

  25. [33]

    Chainlink: https://blog.chain.link/how-to-audit smartcontract. March

  26. [34]

    Lora: Low-rank adaptation of large language models

    Edward J Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen. Lora: Low-rank adaptation of large language models. arXiv preprint arXiv:2106.09685, 2021

    2021 arXiv

  27. [35]

    Zeus: analyzing safety of smart contracts

    Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. Zeus: analyzing safety of smart contracts. In Ndss, 2018

    2018

  28. [36]

    Large language models are zero-shot reasoners

    Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. Large language models are zero-shot reasoners. arXiv preprint arXiv:2205.11916 , 2022

    2022 arXiv

  29. [37]

    Teether: Gnawing at ethereum to automatically exploit smart contracts

    Johannes Krupp and Christian Rossow. Teether: Gnawing at ethereum to automatically exploit smart contracts. In 27th U SEN IXSecurity Symposium, 2018

    2018

  30. [38]

    Lahiri and Shaz Qadeer

    Shuvendu K. Lahiri and Shaz Qadeer. Complexity and algorithms for monomial and clausal predicate abstraction. In Renate A. Schmidt, editor, Automated Deduction – CADE-22 , Berlin, Heidelberg, 2009. Springer Berlin Heidelberg

    2009

  31. [39]

    Powering the static driver verifier using corral

    Akash Lal and Shaz Qadeer. Powering the static driver verifier using corral. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering , FSE 2014, New York, NY , USA, 2014. Association for Computing Machinery

    2014

  32. [40]

    Statically detecting likely buffer overflow vulnerabilities

    David Larochelle and David Evans. Statically detecting likely buffer overflow vulnerabilities. In 2001 USENIX Security Symposium, Washington, DC, 2001

    2001

  33. [41]

    A mathematical investigation of hallucination and creativity in gpt models

    Minhyeok Lee. A mathematical investigation of hallucination and creativity in gpt models. Mathematics, 11(10), 2023

    2023

  34. [42]

    This is boogie 2

    K Rustan M Leino. This is boogie 2. manuscript KRML, 178(131), 2008

    2008

  35. [43]

    Reguard: finding reentrancy bugs in smart contracts

    Chao Liu, Han Liu, Zhao Cao, Zhong Chen, Bangdao Chen, and Bill Roscoe. Reguard: finding reentrancy bugs in smart contracts. In Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings , 2018

    2018

  36. [44]

    Few-shot parameter-efficient fine-tuning is better and cheaper than in-context learning

    Haokun Liu, Derek Tam, Mohammed Muqeeth, Jay Mohta, Tenghao Huang, Mohit Bansal, and Colin A Raffel. Few-shot parameter-efficient fine-tuning is better and cheaper than in-context learning. Advances in Neural Information Processing Systems , 35, 2022

    2022

  37. [45]

    Learning contract invariants using reinforcement learning

    Junrui Liu, Yanju Chen, Bryan Tan, Isil Dillig, and Yu Feng. Learning contract invariants using reinforcement learning. In Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering, 2022

    2022

  38. [46]

    Pre-train, prompt, and predict: A systematic survey of prompting methods in natural language processing

    Pengfei Liu, Weizhe Yuan, Jinlan Fu, Zhengbao Jiang, Hiroaki Hayashi, and Graham Neubig. Pre-train, prompt, and predict: A systematic survey of prompting methods in natural language processing. ACM Computing Surveys, 55(9), 2023

    2023

  39. [47]

    Invcon: A dynamic invariant detector for ethereum smart contracts

    Ye Liu and Yi Li. Invcon: A dynamic invariant detector for ethereum smart contracts. In 37th IEEE/ACM International Conference on Automated Software Engineering , 2022

    2022

  40. [48]

    Neucheck: A more practical ethereum smart contract security analysis tool

    Ning Lu, Bin Wang, Yongxin Zhang, Wenbo Shi, and Christian Esposit. Neucheck: A more practical ethereum smart contract security analysis tool. In Software: Practice and Experience , vol. 51, no. 10, 2021

    2021

  41. [49]

    Making smart contracts smarter

    Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. Making smart contracts smarter. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security . CCS ’16, 2016

    2016

  42. [50]

    Security vulnerabilities in ethereum smart contracts

    Alexander Mense and Markus Flatscher. Security vulnerabilities in ethereum smart contracts. In Proceedings of the 20th international conference on information integration and web-based applications & services, 2018

    2018

  43. [51]

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

    Mark Mossberg, Felipe Manzano, Eric Hennenfent, Alex Groce, Gustavo Grieco, Josselin Feist, Trent Brunson, and Artem Dinaburg. Manticore: A user-friendly symbolic execution framework for binaries and smart contracts. In 2019 34th IEEE/ACM International Conference on Automated ...

    2019

  44. [52]

    sfuzz: An efficient adaptive fuzzer for solidity smart contracts

    Tai D Nguyen, Long H Pham, Jun Sun, Yun Lin, and Quang Tran Minh. sfuzz: An efficient adaptive fuzzer for solidity smart contracts. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering, 2020

    2020

  45. [53]

    Finding the greedy, prodigal, and suicidal contracts at scale

    Ivica Nikoli ´c, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and Aquinas Hobor. Finding the greedy, prodigal, and suicidal contracts at scale. In Proceedings of the 34th annual computer security applications conference, 2018

    2018

  46. [54]

    Finding the greedy, prodigal, and suicidal contracts at scale

    Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and Aquinas Hobor. Finding the greedy, prodigal, and suicidal contracts at scale. In Proceedings of the 34th Annual Computer Security Applications Conference. ACSAC ’18, 2018. 17

    2018

  47. [55]

    Static verification of dynamically detected program invariants: Integrating daikon and esc/java

    Jeremy W Nimmer and Michael D Ernst. Static verification of dynamically detected program invariants: Integrating daikon and esc/java. Electronic Notes in Theoretical Computer Science , 55(2), 2001

    2001

  48. [56]

    Gpt4: https://openai.com/gpt-4

    OpenAI. Gpt4: https://openai.com/gpt-4. 2023

    2023

  49. [57]

    Timelockcontroller

    OpenZeppelin. Timelockcontroller. CVE-2021-39167, Common Vulnerabilities and Exposures Database , 2021

    2021

  50. [58]

    Verx: Safety verification of smart contracts

    Anton Permenev, Dimitar Dimitrov, Petar Tsankov, Dana Drachsler- Cohen, and Martin Vechev. Verx: Safety verification of smart contracts. In 2020 IEEE symposium on security and privacy (SP) . IEEE, 2020

    2020

  51. [59]

    The polynetwork hack explained

    Kudelski Security Research. The polynetwork hack explained. August 2022

    2022

  52. [60]

    Exploring transfer learning with t5: the text-to-text transfer transformer

    Adam Roberts and Colin Raffel. Exploring transfer learning with t5: the text-to-text transfer transformer. March 2022

    2022

  53. [61]

    Cln2inv: learning loop invariants with continuous logic networks

    Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, and Suman Jana. Cln2inv: learning loop invariants with continuous logic networks. arXiv preprint arXiv:1909.11542 , 2019

    1909 arXiv

  54. [62]

    Pods finance ethereum volatility vault audit #1

    Openzeppelin Security. Pods finance ethereum volatility vault audit #1. March 2022

    2022

  55. [63]

    A concurrent perspective on smart contracts

    Ilya Sergey and Aquinas Hobor. A concurrent perspective on smart contracts. In Financial Cryptography and Data Security: FC 2017 International Workshops, WAHC, BITCOIN, VOTING, WTSC, and TA, Sliema, Malta, April 7, 2017, Revised Selected Papers 21 . Springer, 2017

    2017

  56. [64]

    Reentrancy attack: Analysis of visor- finance’s uniswapv3 liquidity protocol hack

    SHARKTEAM. Reentrancy attack: Analysis of visor- finance’s uniswapv3 liquidity protocol hack. Medium: https://sharkteam.org/report/analysis/20211223001A en.pdf, 2021

    2021

  57. [65]

    Smart contract vulnerabilities, attacks and auditing consid- erations

    Maheswar Sharma, Keerthana Kasthuri, Parvinder Singh, and Nynisha Akula. Smart contract vulnerabilities, attacks and auditing consid- erations. In The Auditor’s Guide to Blockchain Technology . CRC Press

  58. [66]

    How long does smart contract audit takes

    Cypher Shield. How long does smart contract audit takes. March 2023

    2023

  59. [67]

    Smartest: Effectively hunting vulnerable transaction sequences in smart contracts through language model-guided symbolic execution

    Sunbeom So, Seongjoon Hong, and Hakjoo Oh. Smartest: Effectively hunting vulnerable transaction sequences in smart contracts through language model-guided symbolic execution. In USENIX Security Symposium, 2021

    2021

  60. [68]

    Verismart: A highly precise safety verifier for ethereum smart contracts

    Sunbeom So, Myungho Lee, Jisu Park, Heejo Lee, and Hakjoo Oh. Verismart: A highly precise safety verifier for ethereum smart contracts. In 2020 IEEE Symposium on Security and Privacy (SP) . IEEE, 2020

    2020

  61. [69]

    Solidity by example: Function selector

  62. [70]

    When gpt meets program analysis: Towards intelligent detection of smart contract logic vulnerabilities in gptscan

    Yuqiang Sun, Daoyuan Wu, Yue Xue, Han Liu, Haijun Wang, Zhengzi Xu, Xiaofei Xie, and Yang Liu. When gpt meets program analysis: Towards intelligent detection of smart contract logic vulnerabilities in gptscan. arXiv preprint arXiv:2308.03314 , 2023

    2023 arXiv

  63. [71]

    Defihacklabs git repository: https://github.com/sunweb3sec/defihacklabs/projects?query=is

    SunWeb3Sec. Defihacklabs git repository: https://github.com/sunweb3sec/defihacklabs/projects?query=is

  64. [72]

    Hashimoto

    Rohan Taori, Ishaan Gulrajani, Tianyi Zhang, Yann Dubois, Xuechen Li, Carlos Guestrin, Percy Liang, and Tatsunori B. Hashimoto. Stanford alpaca: An instruction-following llama model. March 2022

    2022

  65. [73]

    Confuzzius: A data dependency-aware hybrid fuzzer for smart contracts

    Christof Ferreira Torres, Antonio Ken Iannillo, Arthur Gervais, and Radu State. Confuzzius: A data dependency-aware hybrid fuzzer for smart contracts. In 2021 IEEE European Symposium on Security and Privacy (EuroS&P). IEEE, 2021

    2021

  66. [74]

    Osiris: Hunting for integer bugs in ethereum smart contracts

    Christof Ferreira Torres, Julian Sch ¨utte, and Radu State. Osiris: Hunting for integer bugs in ethereum smart contracts. In Proceedings of the 34th Annual Computer Security Applications Conference , 2018

    2018

  67. [75]

    The art of the scam: Demystifying honeypots in ethereum smart contracts

    Christof Ferreira Torres, Mathis Steichen, and Radu State. The art of the scam: Demystifying honeypots in ethereum smart contracts. In Proceedings of the 28th USENIX Conference on Security Symposium . 2019

    2019

  68. [76]

    Llama: Open and efficient foundation language models

    Hugo Touvron, Thibaut Lavril, Gautier Izacard, Xavier Martinet, Marie-Anne Lachaux, Timoth ´ee Lacroix, Baptiste Rozi `ere, Naman Goyal, Eric Hambro, Faisal Azhar, Aurelien Rodriguez, Armand Joulin, Edouard Grave, and Guillaume Lample. Llama: Open and efficient foundation lang...

    2023

  69. [77]

    Detecting nondeter- ministic payment bugs in ethereum smart contracts

    Shuai Wang, Chengyu Zhang, and Zhendong Su. Detecting nondeter- ministic payment bugs in ethereum smart contracts. Proceedings of the ACM on Programming Languages , 3(OOPSLA), 2019

    2019

  70. [78]

    Formal verification of workflow policies for smart contracts in azure blockchain

    Yuepeng Wang, Shuvendu K Lahiri, Shuo Chen, Rong Pan, Isil Dillig, Cody Born, Immad Naseer, and Kostas Ferles. Formal verification of workflow policies for smart contracts in azure blockchain. In Verified Software. Theories, Tools, and Experiments: 11th International Conferenc...

    2019

  71. [79]

    Emergent abilities of large language models

    Jason Wei, Yi Tay, Rishi Bommasani, Colin Raffel, Barret Zoph, Sebastian Borgeaud, Dani Yogatama, Maarten Bosma, Denny Zhou, Donald Metzler, et al. Emergent abilities of large language models. arXiv preprint arXiv:2206.07682 , 2022

    2022 arXiv

  72. [80]

    Chain of thought prompting elicits reasoning in large language models

    Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Ed Chi, Quoc Le, and Denny Zhou. Chain of thought prompting elicits reasoning in large language models. arXiv preprint arXiv:2201.11903, 2022

    2022 arXiv

  73. [81]

    A prompt pattern catalog to enhance prompt engineering with chatgpt

    Jules White, Quchen Fu, Sam Hays, Michael Sandborn, Carlos Olea, Henry Gilbert, Ashraf Elnashar, Jesse Spencer-Smith, and Douglas C Schmidt. A prompt pattern catalog to enhance prompt engineering with chatgpt. arXiv preprint arXiv:2302.11382 , 2023

    2023 arXiv

  74. [82]

    Defiranger: Detecting price manip- ulation attacks on defi applications

    Siwei Wu, Dabao Wang, Jianting He, Yajin Zhou, Lei Wu, Xingliang Yuan, Qinming He, and Kui Ren. Defiranger: Detecting price manip- ulation attacks on defi applications. arXiv preprint arXiv:2104.15068 , 2021

    2021 arXiv

  75. [83]

    Finding consensus bugs in ethereum via multi-transaction differential fuzzing

    Youngseok Yang, Taesoo Kim, and Byung-Gon Chun. Finding consensus bugs in ethereum via multi-transaction differential fuzzing. In OSDI, pages 349–365, 2021

    2021

  76. [84]

    Learning nonlinear loop invariants with gated continuous logic networks

    Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, and Ronghui Gu. Learning nonlinear loop invariants with gated continuous logic networks. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation , 2020

    2020

  77. [85]

    Svchecker: a deep learning-based system for smart contract vulnerability detection

    Ye Yuan and TongYi Xie. Svchecker: a deep learning-based system for smart contract vulnerability detection. In Proceedings Volume 12260, International Conference on Computer Application and Information Security. ICCAIS, 2021

    2021

  78. [86]

    Xscope: Hunting for cross-chain bridge attacks

    Jiashuo Zhang, Jianbo Gao, Yue Li, Ziming Chen, Zhi Guan, and Zhong Chen. Xscope: Hunting for cross-chain bridge attacks. In 37th IEEE/ACM International Conference on Automated Software Engineering. ICSE’22, 2022

    2022

  79. [87]

    Machine learning topological invariants with neural networks

    Pengfei Zhang, Huitao Shen, and Hui Zhai. Machine learning topological invariants with neural networks. Physical review letters, 120(6)

  80. [88]

    Opt: Open pre-trained transformer language models

    Susan Zhang, Stephen Roller, Naman Goyal, Mikel Artetxe, Moya Chen, Shuohui Chen, Christopher Dewan, Mona Diab, Xian Li, Xi Victoria Lin, Todor Mihaylov, Myle Ott, Sam Shleifer, Kurt Shuster, Daniel Simig, Punit Singh Koura, Anjali Sridhar, Tianlu Wang, and Luke Zettlemoyer. O...

    2022

  81. [89]

    Generalized cross entropy loss for training deep neural networks with noisy labels

    Zhilu Zhang and Mert Sabuncu. Generalized cross entropy loss for training deep neural networks with noisy labels. Advances in neural information processing systems , 31, 2018

    2018

  82. [90]

    Demystifying exploitable bugs in smart contracts

    Zhuo Zhang, Brian Zhang, Wen Xu, and Zhiqiang Li. Demystifying exploitable bugs in smart contracts. In Proceedings of nternational Conference on Software Engineering . ICSE’23, 2023

    2023

  83. [91]

    Smart contract vulnerability detection using graph neural networks

    Yuan Zhuang, Zhenguang Liu, Peng Qian, Qi Liu, Xiang Wang, and Qinming He. Smart contract vulnerability detection using graph neural networks. In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence . IJCAI’20, 2020. 18 Appendix A. Meta-Rev...

    2020

Pith tools

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