Automated Invariant Generation for Solidity Smart Contracts

Chengxuan Zhang; Singapore); Ye Liu; Yi Li. (Nanyang Technological University

Automated Invariant Generation for Solidity Smart Contracts

Not yet reviewed by Pith; the record is open.

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

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2401.00650 v1 pith:BJSP5FFW submitted 2024-01-01 cs.SE

Ye Liu , Chengxuan Zhang , Yi Li. (Nanyang Technological University , Singapore) This is my paper · ORCID

classification cs.SE

keywords invconcontractssmartcontractinvariantinvariantscodecommon

verification ladder T0 review T1 audit T2 compute T3 formal

0 comments

read the original abstract

Smart contracts are computer programs running on blockchains to automate the transaction execution between users. The absence of contract specifications poses a real challenge to the correctness verification of smart contracts. Program invariants are properties that are always preserved throughout the execution, which characterize an important aspect of the program behaviors. In this paper, we propose a novel invariant generation framework, INVCON+, for Solidity smart contracts. INVCON+ extends the existing invariant detector, InvCon, to automatically produce verified contract invariants based on both dynamic inference and static verification. Unlike INVCON+, InvCon only produces likely invariants, which have a high probability to hold, yet are still not verified against the contract code. Particularly, INVCON+ is able to infer more expressive invariants that capture richer semantic relations of contract code. We evaluate INVCON+ on 361 ERC20 and 10 ERC721 real-world contracts, as well as common ERC20 vulnerability benchmarks. The experimental results indicate that INVCON+ efficiently produces high-quality invariant specifications, which can be used to secure smart contracts from common vulnerabilities.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Towards LLM-assisted High-Quality Property Generation for Solidity Smart Contracts
cs.SE 2026-07 conditional novelty 4.0 of 10

LLM-generated Solidity test properties catch most of the mutants that human-written properties catch on average, and match human quality on the LibBit contract.

Pith tools