Pith. sign in

REVIEW 3 major objections 2 minor 35 references

Constructing Trustworthy Smart Contracts

T0 review · 3 major / 2 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 This paper introduces Asp, a smart-contract language whose safety proofs carry over to the compiled Solidity code, so that security can be verified before deployment.

desk verdict A well-written smart-contract language design whose central compilation-correctness guarantee is asserted, not proved, making the paper a promising proposal rather than a demonstrated system. read the letter →

arxiv 2411.14563 v1 pith:ACKPZHSN submitted 2024-11-21 cs.CR cs.PL

Devora Chait-Roth , Kedar S. Namjoshi This is my paper · ORCID
classification cs.CRcs.PL
keywords AspsmartcontractsdeductiveverificationdefensivecompilationreentrancysafetypropertiesSolidityfinite-statemachines
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

The paper introduces Asp, a language for writing smart contracts that are provably secure. Asp contracts are finite-state machines over abstract types—coins, tokens, addresses, timers—whose semantics rule out arithmetic overflow, out-of-bounds access, and reentrancy. A defensive compiler translates Asp to Solidity, inserting runtime checks that enforce the abstract semantics, and a proof checker verifies safety and liveness properties through deductive proofs. The central claim is that every safety property proved at the Asp level is also a safety property of the deployed Solidity code, because every successful compiled transaction corresponds to a valid Asp cascade. If true, this would mean contract security can be established once, at the level of a simple language, rather than re-proved for each target blockchain.

What carries the argument

The central mechanism is the combination of Asp's state-machine language over abstract data types, the cascade execution semantics, and the defensive compiler. The cascade semantics defines execution as a sequence of synchronized message exchanges starting from a quiescent configuration, using a pushdown stack of contract indices with at most R+1 occurrences of each index; R=1 blocks malicious reentrancy. The proof checker uses ghost variables and rank functions to discharge safety and reachability obligations, with lemmas checked by Viper/SMT.

What would settle it

A transaction of a compiled Asp contract that succeeds on the EVM but whose corresponding sequence of Asp transitions is not a valid cascade under the paper's semantics—for instance, a reentrant call into the same contract twice within one transaction that nevertheless commits—would refute Property 1. Concretely, one could instrument a compiled auction or EtherStore contract and attempt the classic reentrancy attack, checking whether the reentrancy counter ever allows a second reentry.

Watch

Extended reading notes

Core claim

The paper's central claim is Property 1: for Asp contracts C1...Cn and their compiled Solidity counterparts S1...Sn, every successful transaction of the compiled contracts corresponds to a successful cascade of the Asp contracts. As a corollary, every safety property of an Asp contract is a safety property of the compiled contract. The argument rests on a cascading, single-threaded execution semantics for Asp that is deliberately designed to mirror EVM transaction execution, with a pushdown stack and a reentrancy limit R=1 that blocks the classic reentrancy attack while still allowing one message-response exchange. The defensive compiler enforces this semantics by checking guards, reverting on undefined operations, and inserting a reentrancy counter.

Load-bearing premise

The cascade semantics, including the pushdown stack and the reentrancy limit, is assumed to match how the compiled Solidity actually executes on the Ethereum Virtual Machine, including reverts and the inserted reentrancy counter, but the paper gives no formal proof of that match.

Editorial extensions

If this is right

  • A safety property proved on an Asp contract does not need to be re-proved for the compiled Solidity code, assuming the defensive compiler preserves the cascade semantics.
  • The reentrancy limit of one allows a message-response interaction but blocks the unlimited reentrancy used in DAO-style attacks.
  • Because arithmetic is mathematical in Asp, overflow and undefined operations are handled by runtime defensive checks that revert the transaction, so the programmer can ignore them.
  • The same verified Asp contract can be ported to multiple blockchains (e.g., Ink!/Rust) by recompiling, without redoing proofs.
  • Deductive proofs are independently checkable by any participant, which fits the trustless Web3 setting.

Reading between the lines

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

  • A formal connection between the cascade semantics and a concrete EVM semantics (e.g., KEVM) would turn the paper's correctness claim into a machine-checked theorem; the paper leaves this as the key missing link.
  • The safety-transfer result might be extended to adversarial liveness only under an assumption that overflow and gas exhaustion never cause reverts; under that assumption the paper claims a bisimulation.
  • The reentrancy limit of one may rule out legitimate contracts that require deeper call chains, suggesting a parameterized R or a more refined access-control mechanism as a future direction.
  • The design could be applied to other security properties by adding new abstract types, such as commitments or randomness, which the paper explicitly mentions as planned work.
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 / 2 minor

Summary. The paper presents Asp, a smart-contract development system combining a high-level state-machine language with abstract data types (coins, tokens, timers, addresses), a defensive compiler that translates Asp to Solidity with runtime checks against overflow, undefined operations, coin-conservation and reentrancy, and a proof checker that verifies user-supplied safety, reachability, and adversarial-liveness properties by translation to Viper. The central claimed guarantee is Property 1 in Section 5: every successful transaction of the compiled contracts corresponds to a successful cascade of the Asp contracts, with the corollary that safety properties proved at the Asp level transfer to the deployed Solidity. The paper illustrates the language on an auction, a token bank, an Ether store, and a vending machine, and describes a prototype implementation.

Significance. If the central guarantee were established, Asp would be a significant contribution to the smart-contract verification literature: it offers a clean state-machine model, a library of high-level abstractions that eliminate entire classes of vulnerabilities by construction, a path to deductive verification using the existing Viper infrastructure, and a compiler that ports verified contracts to mainstream blockchains. The paper is generally clear and the examples are instructive. The prototype and the public example contracts are strengths, and the proof rules for safety and timer-based reachability are standard and plausible. However, the load-bearing compilation-correctness theorem is stated without proof, and the reentrancy-blocking claim is not correctly argued; these gaps prevent the paper from establishing its headline trust guarantee.

major comments (3)
  1. [Section 5, Property 1] Property 1 is the sole bridge between Asp-level proofs and guarantees about the compiled Solidity, but no proof is provided. The preceding paragraphs describe the compiler informally (messages to public methods, a private tau_closure method, low-level calls, and an inserted reentrancy counter) without defining a simulation relation between compiled Solidity states and Asp configurations, without showing that the reentrancy counter exactly enforces the recurrence limit R=1, and without relating Solidity call/return/revert behavior to the pushdown cascade semantics. The corollary that every Asp safety property is a safety property of the compiled contract therefore rests on an unproven assumption, as the paper itself acknowledges with 'assuming correct compilation.' This is a load-bearing gap for the paper's central claim.
  2. [Section 3.2 and Appendix A] The claim that 'Reentrancy attacks are blocked with R = 1 as it is impossible for an attacker contract to trigger an account withdrawal transition twice within a cascade' is not proven, and the illustrative trace in Appendix A misattributes the blocking of the attack. In the step-5 configuration the stack is [Attacker, Etherstore, Attacker]; at step 6, the attempted reentrant push is impossible because Etherstore is in ResetBalance, which has no matching input transition, not because the recurrence limit is exceeded. Indeed, with R=1 the semantics allows up to two occurrences of an index on the stack (as the trace itself shows with Attacker), so the statement that a withdrawal transition cannot be triggered twice is false as written. A precise security definition and a proof are needed, not an informal assertion.
  3. [Section 5, final paragraph] The paper first says compilation correctness is expressed as a language inclusion, then in the final paragraph claims the reverse direction ('every Asp contract cascade is matched by a successful transaction of the compiled code') and 'induces a bisimulation,' with no proof. This is a much stronger statement than Property 1 and is also needed for the claimed transfer of adversarial liveness and reachability properties. The qualifier 'under the assumption that arithmetic overflow or shortage of gas do not cause a transaction to revert' is not formalized; the Asp semantics does not model gas, so the condition cannot be checked or verified.
minor comments (2)
  1. [Throughout] The text contains several broken word-spacing artifacts (e.g., 'inAsp' on page 5, 'theAsp' on page 3) and inconsistent code-label spacing in figures (e.g., 'ma xB id de r' in Figure 3); these should be cleaned up.
  2. [Sections 4.3 and Appendix B] The proof rule and soundness argument for adversarial liveness appear in both Section 4.3 and Appendix B with only minor differences; this duplication should be consolidated to avoid confusion about which proof system is implemented.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the verification rules are presented with soundness arguments, and the main compilation-correctness assumption, while unproved, is not a circular reduction.

full rationale

The paper's derivation chain is largely self-contained. The safety proof method is the standard automaton/product construction, and the paper proves the equivalence between safety of a computation and non-reachability of a rejecting automaton state. The timer-based reachability proof rule is accompanied by a direct soundness proof using well-founded ranks. The adversarial liveness proof rule is likewise justified by a soundness argument and a µ-calculus completeness framing; the citation to the second author's prior work is for inspiration only and is not the load-bearing justification. The language-level guarantees against overflow, out-of-bounds access, and reentrancy hold by construction of the Asp semantics and the inserted defensive checks, so they are not fitted inputs or self-referential predictions. The most significant potential concern is Property 1, the compilation-correctness assertion that every successful compiled transaction corresponds to a successful Asp cascade. This property is stated without proof, and the paper explicitly relies on 'assuming correct compilation' when transferring safety properties. That is a genuine evidential gap in the compilation argument, but it is not circularity: the paper does not define the compiled semantics so as to make the property true by definition, nor does it fit a parameter and then rename the fit as a prediction. Under the hard rule that circularity must be exhibited as a specific reduction, no circular step can be identified. Accordingly, the circularity score is 0.

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

The Asp design introduces abstract types (Coin, Token, Timer) and ghost variables as new constructs, but their safety guarantees rest on unproven assumptions about the compiler, the cascade semantics, and the Viper verifier. The main free design parameter is the reentrancy limit R, set to 1 without a general proof that this blocks all attacks.

free parameters (1)
  • Reentrancy limit R = 1
    The cascade semantics is parameterized by a recurrence limit R; the paper sets R=1 to block reentrancy. This is a hand-chosen design parameter, not fitted to data, but the security guarantee depends on it.
assumptions (5)
  • domain assumption Mathematical (unbounded) integer arithmetic in Asp must be enforced at run time in compiled Solidity; overflow must cause a revert, consistent with language inclusion.
    Section 2.2 calls the mathematical arithmetic a 'fiction'; Section 5 relies on this for Property 1.
  • domain assumption The cascade semantics with pushdown stack and recurrence limit R faithfully models the EVM execution of compiled contracts.
    Section 3.2 defines the semantics; Property 1 in Section 5 assumes the correspondence without proof.
  • domain assumption The reentrancy counter inserted by the compiler correctly enforces the R=1 limit in the compiled code.
    Section 5 describes the counter; its correctness is not proven.
  • domain assumption The Viper verifier is sound for the generated lemmas and Hoare triples.
    Section 4 relies on Viper for all proof checking; Viper is external and not formally verified in this paper.
  • domain assumption Transactions that revert on the blockchain leave state unchanged.
    Standard EVM behavior relied upon in Section 5 to reconcile reverts with the Asp semantics.
invented entities (4)
  • Coin abstract type
    purpose: Represents native cryptocurrency in a way that enforces conservation: coins cannot be created or destroyed, only transferred.
    The type is defined in the paper (Section 2.2) and enforced by the type system and compiler. No independent artifact or external benchmark is provided.
  • Token abstract type
    purpose: Represents issuer-defined tokens with issue, burn, and transfer operations, intended to prevent honeypot scams.
    Defined in Section 2.2. The paper provides a code snippet but no independent verification.
  • Timer abstract type
    purpose: Models blockchain time as non-deterministic advancement, used to prove reachability and liveness properties.
    Defined in Section 2.2 and used in the reachability proof example; the soundness of the timer model depends on the informal semantics.
  • Ghost variables
    purpose: Auxiliary proof state that encodes a deterministic violation automaton for safety proofs.
    Introduced in Section 4.1. The type checker enforces non-interference, but the verification of this enforcement is not formally proved.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Constructing Trustworthy Smart Contracts." pith.science (2026). https://pith.science/paper/ACKPZHSN

@misc{pith2026241114563,
  author       = {Pith},
  title        = {Pith review of: Constructing Trustworthy Smart Contracts},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ACKPZHSN}},
  note         = {Machine review of arXiv:2411.14563}
}
read the original abstract

Smart contracts form the core of Web3 applications. Contracts mediate the transfer of cryptocurrency, making them irresistible targets for hackers. We introduce ASP, a system aimed at easing the construction of provably secure contracts. The Asp system consists of three closely-linked components: a programming language, a defensive compiler, and a proof checker. The language semantics guarantee that Asp contracts are free of commonly exploited vulnerabilities such as arithmetic overflow and reentrancy. The defensive compiler enforces the semantics and translates Asp to Solidity, the most popular contract language. Deductive proofs establish functional correctness and freedom from critical vulnerabilities such as unauthorized access.

Figures

Figures reproduced from arXiv: 2411.14563 by the authors.

Figure 1
Figure 1. The Asp pipeline. The Viper system is used to verify proof assertions. This paper introduces the Asp system, which is aimed at easing the construc￾tion of provably secure contracts while addressing these drawbacks. It has three tightly-linked components, as shown in [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Skeleton of an open auction contract in Asp [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Code snippets of open auction contract and receiving contract in Asp [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Open auction contract with ghost variables [PITH_FULL_IMAGE:figures/full_fig_p014_4.png]
Figure 5
Figure 5. Figure 5: Two contracts that demonstrate limited reentrancy in [PITH_FULL_IMAGE:figures/full_fig_p025_5.png]
Figure 6
Figure 6. Figure 6: A Vending Machine contract outline. value 0 at the Wait state, value 2 for the Choose state with a defined customer, and value 1 at the Deliver state. Consider a customer x. If the machine is at the Wait state, then Q holds, as pay is enabled for x. If the machine is a…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

35 extracted references · 33 canonical work pages

  1. [1]

    At https://www.cnbc.com/2023/02/04/ crypto-investors-lost-nearly-4-billion-dollars-to-hackers-in-2022

    Crypto investors lost nearly $4 billion to hack- ers in 2022. At https://www.cnbc.com/2023/02/04/ crypto-investors-lost-nearly-4-billion-dollars-to-hackers-in-2022. html

    work page 2022

  2. [2]

    At https://www.certik.com/resources/ blog/7BokMhPUgffqEvyvXgHNaq-hack3d-the-web3-security-report-2023

    Hack3d: The web3 security report 2023. At https://www.certik.com/resources/ blog/7BokMhPUgffqEvyvXgHNaq-hack3d-the-web3-security-report-2023

    work page 2023

  3. [3]

    At https://docs

    SMTChecker and Formal Verification for Solidity. At https://docs. soliditylang.org/en/v0.8.23/smtchecker.html

    work page

  4. [4]

    Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181–185 (1985)

    work page 1985

  5. [5]

    In: FM Workshops (1)

    Bernardo, B., Cauderlier, R., Hu, Z., Pesin, B., Tesson, J.: Mi-Cho-Coq, a Frame- work for Certifying Tezos Smart Contracts. In: FM Workshops (1). Lecture Notes in Computer Science, vol. 12232, pp. 368–379. Springer (2019)

    work page 2019

  6. [6]

    Blackshear, S., Cheng, E., Dill, D.L., Gao, V., Maurer, B., Nowacki, T., Pott, A., Qadeer, S., Rain, Russi, D., Sezer, S., Zakian, T., Zhou, R.: Move: A Language With Programmable Resources, https://developers.diem.com/papers/diem-move- a-language-with-programmable-resources/2019-06-18.pdf

    work page 2019

  7. [7]

    Br¨ am, C., Eilers, M., M¨ uller, P., Sierra, R., Summers, A.J.: Rich specifications for Ethereum smart contract verification. Proc. ACM Program. Lang. 5(OOPSLA), 1–30 (2021)

    work page 2021

  8. [8]

    In: FMICS

    Cassez, F., Fuller, J., Quiles, H.M.A.: Deductive verification of smart contracts with dafny. In: FMICS. Lecture Notes in Computer Science, vol. 13487, pp. 50–66. Springer (2022)

    work page 2022

Show all 35 references
  1. [9]

    ACM Trans

    Coblenz, M., Oei, R., Etzel, T., Koronkevich, P., Baker, M., Bloem, Y., My- ers, B.A., Sunshine, J., Aldrich, J.: Obsidian: Typestate and assets for safer blockchain programming. ACM Trans. Program. Lang. Syst. 42(3) (Nov 2020). https://doi.org/10.1145/3417516, https://doi.org...

    2020 doi

  2. [10]

    In: TACAS (1)

    Dill, D.L., Grieskamp, W., Park, J., Qadeer, S., Xu, M., Zhong, J.E.: Fast and Reliable Formal Verification of Smart Contracts with the Move Prover. In: TACAS (1). Lecture Notes in Computer Science, vol. 13243, pp. 183–200. Springer (2022)

    2022

  3. [11]

    In: Chakraborty, S., Navas, J.A

    Hajdu, ´A., Jovanovi´ c, D.: solc-verify: A modular verifier for Solidity smart con- tracts. In: Chakraborty, S., Navas, J.A. (eds.) Verified Software. Theories, Tools, and Experiments, Lecture Notes in Computer Science, vol. 12301, pp. 161–179. Springer (2020)

    2020

  4. [12]

    Hildenbrandt, E., Saxena, M., Rodrigues, N., Zhu, X., Daian, P., Guth, D., Moore, B.M., Park, D., Zhang, Y., Stefanescu, A., Rosu, G.: KEVM: A complete formal semantics of the ethereum virtual machine. In: CSF. pp. 204–217. IEEE Computer Society (2018)

    2018

  5. [13]

    In: Financial Cryptography

    Mavridou, A., Laszka, A.: Designing Secure Ethereum Smart Contracts: A Fi- nite State Machine Based Approach. In: Financial Cryptography. Lecture Notes in Computer Science, vol. 10957, pp. 523–540. Springer (2018)

    2018

  6. [14]

    In: Financial Cryptography

    Mavridou, A., Laszka, A., Stachtiari, E., Dubey, A.: VeriSolid: Correct-by-Design Smart Contracts for Ethereum. In: Financial Cryptography. Lecture Notes in Com- puter Science, vol. 11598, pp. 446–465. Springer (2019)

    2019

  7. [15]

    In: VMCAI

    M¨ uller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. In: VMCAI. Lecture Notes in Computer Science, vol. 9583, pp. 41–62. Springer (2016) 21

    2016

  8. [16]

    In: CA V

    Namjoshi, K.S.: Certifying model checkers. In: CA V. Lecture Notes in Computer Science, vol. 2102, pp. 2–13. Springer (2001)

    2001

  9. [17]

    In: POPL

    Necula, G.C.: Proof-carrying code. In: POPL. pp. 106–119. ACM Press (1997)

    1997

  10. [18]

    In: FSTTCS

    Peled, D.A., Pnueli, A., Zuck, L.D.: From falsification to verification. In: FSTTCS. Lecture Notes in Computer Science, vol. 2245, pp. 292–304. Springer (2001)

    2001

  11. [19]

    In: IEEE Symposium on Security and Pri- vacy (2020)

    Permenev, A., Dimitrov, D., Tsankov, P., Drachsler-Cohen, D., Vechev, M.: Verx: Safety verification of smart contracts. In: IEEE Symposium on Security and Pri- vacy (2020)

    2020

  12. [20]

    Sergey, I., Nagaraj, V., Johannsen, J., Kumar, A., Trunov, A., Hao, K.C.G.: Safer smart contract programming with Scilla. Proc. ACM Program. Lang.3(OOPSLA), 185:1–185:30 (2019)

    2019

  13. [21]

    In: IEEE Symposium on Secu- rity and Privacy (2021)

    Stephens, J., Ferles, K., Mariano, B., Lahiri, S., Dillig, I.: Smartpulse: Automated checking of temporal properties in smart contracts. In: IEEE Symposium on Secu- rity and Privacy (2021)

    2021

  14. [22]

    In: PriSC (2024), at https://arxiv.org/pdf/2311

    Sun, H., Singh, K., Ramos-D´ avila, J.P., Aldrich, J., DiVincenzo, J.: Gradual ver- ification for smart contracts. In: PriSC (2024), at https://arxiv.org/pdf/2311. 13351.pdf

    2024

  15. [23]

    In: CA V (1)

    Zhong, J.E., Cheang, K., Qadeer, S., Grieskamp, W., Blackshear, S., Park, J., Zohar, Y., Barrett, C.W., Dill, D.L.: The Move Prover. In: CA V (1). Lecture Notes in Computer Science, vol. 12224, pp. 137–150. Springer (2020) 22 A Cascade semantics and reentrancy The cascade sema...

    2020

  16. [24]

    Attacker is pushed onto the stack, and Attacker’s state is updated to CollectDeposit

    Environment Input, via Attacker . Attacker is pushed onto the stack, and Attacker’s state is updated to CollectDeposit

  17. [25]

    Etherstore is pushed onto the stack

    Synchronized Push. Etherstore is pushed onto the stack. Attacker’s state is updated to Etherstore Deposit, and Etherstore’s state is updated to Accept- Deposit

  18. [26]

    Attacker is now at the top of the stack

    Pop. Attacker is now at the top of the stack

  19. [27]

    Etherstore is pushed onto the stack

    Synchronized Push . Etherstore is pushed onto the stack. Attacker’s state is updated to EtherstoreWithdraw, and Etherstore’s state is updated to WithdrawRequested

  20. [28]

    Attacker is pushed onto the stack (with Attacker at the bottom of the stack as well)

    Synchronized Push. Attacker is pushed onto the stack (with Attacker at the bottom of the stack as well). Since R = 1, this is allowed. Attacker’s state is updated to AcceptReturn, and Etherstore’s state is updated to ResetBal- ance

  21. [29]

    Note that this is where Attacker attempts to maliciously reenter Ether- store

    Pop. Note that this is where Attacker attempts to maliciously reenter Ether- store. This reentrancy is blocked, because the limit of R = 1 is exceeded. Attacker is popped off the stack

  22. [30]

    Etherstore’s state is up- dated to GaveWithdrawal, and then to AcceptDeposit

    Local τ -Move, followed by another Local τ -Move. Etherstore’s state is up- dated to GaveWithdrawal, and then to AcceptDeposit

  23. [31]

    Etherstore is popped off the stack

    Pop. Etherstore is popped off the stack

  24. [32]

    Attacker is prevented from requesting another withdrawal, since its balance has already been reset

    Pop. Attacker is prevented from requesting another withdrawal, since its balance has already been reset. Attacker is therefore popped off the stack, and we return to a quiescent configuration. The reentrancy limit allows for an exchange of message and response, but prevents th...

  25. [33]

    θ is an invariant of the contract M ,

  26. [34]

    ρ is defined for all states in θ, and

  27. [35]

    The soundness of this proof rule is established as follows

    For every state s in θ, one of the following holds: (a) s satisfies q, or (b) There is a transition for the Player to a state s′ that is in θ, and the rank decreases strictly after that transition, or (c) Some Opponent transition is enabled and all Opponent transitions lead to...

Pith tools

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