Pith. sign in

REVIEW 1 cited by

Formal Specification and Verification of Smart Contracts for Azure Blockchain

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 1812.08829 v2 pith:EM3L42EN submitted 2018-12-20 cs.PL

Yuepeng Wang , Shuvendu K. Lahiri , Shuo Chen , Rong Pan , Isil Dillig , Cody Born , Immad Naseer This is my paper · ORCID
classification cs.PL
keywords contractssmartazureblockchainbugsemphensuringformal
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

Ensuring correctness of smart contracts is paramount to ensuring trust in blockchain-based systems. This paper studies the safety and security of smart contracts in the \emph{Azure Blockchain Workbench}, an enterprise Blockchain-as-a-Service offering from Microsoft. As part of this study, we formalize \emph{semantic conformance} of smart contracts against a state machine model with access-control policy and develop a highly-automated formal verifier for Solidity that can produce proofs as well as counterexamples. We have applied our verifier {\sc VeriSol} to analyze {\it all} contracts shipped with the Azure Blockchain Workbench, which includes application samples as well as a governance contract for Proof of Authority (PoA). We have found previously unknown bugs in these published smart contracts. After fixing these bugs, {\sc VeriSol} was able to successfully perform full verification for all of these contracts.

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

  1. 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