{"id":"d4955878-0959-4ec6-9db6-eb0d0bd511db","arxiv_id":"2411.14563","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"high","formal_verification":"none","parameter_count":1,"one_line_summary":"Asp is a state-machine language with abstract coin and timer types, compiled to Solidity with defensive checks, plus a deductive proof checker.","lead":"This paper introduces Asp, a three-part system: a special language for writing smart contracts, a compiler that adds safety checks, and a proof checker. The authors' goal is to make it easy to prove a contract is safe before trusting it with cryptocurrency.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Property 1, the compilation-correctness theorem on which the safety-transfer guarantee rests, is asserted without proof; no simulation relation connects compiled Solidity to the cascade semantics.","rationale":"The paper's contribution is a language/compiler/proof-checker stack whose headline guarantee is: prove safety at the Asp level, and the deployed Solidity is safe. That guarantee is exactly the corollary to Property 1 in Section 5. Reading the paper, Property 1 is introduced after an informal description of the compiler with no proof. There is no formal statement of the translation relation, no invariant, no induction. The surrounding text even says 'assuming correct compilation,' which is the very assumption at issue. This is not a mere presentational gap: the cascade semantics of Section 3.2 is a precise pushdown model, but the compiler description (messages to public methods, tau_closure, low-level calls, reentrancy counter) is not connected to that model at any level of rigor. The claimed safety transfer is the entire basis for the system's trust story, so without a proof, the paper does not substantiate its central claim. The reader's weakest_assumption identifies the same region: the cascade semantics is assumed to faithfully model EVM execution, with no link such as KEVM. I agree with the diagnosis; my sharper formulation is that the unproved step is not merely the external EVM semantics but the compiler's own correctness: even granting the cascade model, nothing shows the generated Solidity implements it. The reentrancy counter, for example, is described as a global check-in/check-out, whereas the cascade model imposes a per-contract occurrence limit on a pushdown stack; whether these coincide (including edge cases around reverts and low-level calls) is never argued. Likewise, the mapping of abstract types (coins, timers, tokens) and ghost variables to Solidity representations, and the preservation of safety-relevant observables, is not formalized. I concur with the reader's verdict of REJECT: the paper is clearly written and presents an interesting design, but the central correctness claim is unsupported. The artifact is not released, so the absence of proof is not mitigated by direct experimental validation. The concrete test I propose—formally proving or disproving Property 1 via a simulation relation between the compiled code and the cascade semantics—would settle whether the concern lands. Until then, the safety-transfer guarantee must be regarded as unverified.","tokens_in":17648,"tokens_out":8484,"duration_ms":81864,"concrete_test":"Formalize the compiler as a translation function from Asp contracts to Solidity/Yul bytecode and prove Property 1 as a theorem relating the cascade semantics of §3.2 to KEVM [12] executions, ideally with a machine-checked proof (e.g., in Lean or Coq). The proof must exhibit a simulation relation covering all five cascade rules, the tau_closure loop, and the reentrancy counter. If no such proof can be constructed, or a counterexample is found where a successful compiled transaction has no matching Asp cascade, the safety-transfer corollary is unsupported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 5 states Property 1: 'Every successful transaction of the compiled contracts corresponds to a successful cascade of the Asp contracts,' and derives the corollary that every Asp safety property is a safety property of the compiled contract. This is the sole bridge between proofs at the Asp level and guarantees about deployed Solidity. Yet the paper gives no proof. The preceding paragraphs describe the compiler informally: messages become public methods, a private tau_closure method repeats τ transitions, sends become low-level calls, and a reentrancy counter is inserted. Nothing establishes that this translation implements the pushdown cascade semantics of Section 3.2. In particular, there is no defined simulation relation between compiled Solidity states and Asp configurations, no proof that the reentrancy counter exactly enforces the recurrence limit R=1, no treatment of how Solidity call-return and revert semantics align with synchronized push/pop transitions, and no formal condition connecting Asp state variables and ghost variables to their Solidity representations. The paper's own corollary says 'assuming correct compilation,' but correctness of compilation is exactly what must be shown. Thus the headline claim that safety proofs at the Asp level carry over to the compiled contract is a claim-without-derivation. The absence is not a matter of EVM detail only: even if the cascade semantics were perfectly faithful to the EVM, the compiler's implementation is not proven to realize it.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":17878,"tokens_out":10870,"duration_ms":98923,"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":[{"comment":"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.","section":"Section 5, Property 1"},{"comment":"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.","section":"Section 3.2 and Appendix A"},{"comment":"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.","section":"Section 5, final paragraph"}],"minor_comments":[{"comment":"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.","section":"Throughout"},{"comment":"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.","section":"Sections 4.3 and Appendix B"}],"recommendation":"reject","confidential_remarks":"The manuscript is an interesting systems paper, but the central compilation-correctness theorem is unproved, and the reentrancy example has a technical error. The authors may be able to resubmit a revised version that either provides a rigorous proof of Property 1 (with a precise simulation relation) or explicitly re-scopes the paper to describe the Asp system without claiming safety transfer to deployed code. Given the current claims, I cannot recommend acceptance."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe Asp paper is a genuinely interesting design proposal with a hole where the main theorem should be. If you read it as a systems paper about language abstractions and defensive compilation, it's well done. If you read the headline claim as a formal guarantee, it's not there yet.\n\nWhat's new: Asp wraps a finite-state machine contract language around abstract coin, token, timer types, then compiles to Solidity while inserting runtime checks to enforce the abstraction (overflow, reentrancy, coin conservation). The proof checker translates user proof sketches to Viper. The abstract types are a nice idea—they make conservation properties explicit instead of leaving them to integer accounting. The examples, especially the auction and the reentrancy trace in Appendix A, are clear and instructive.\n\nThe paper also does honest positioning against prior work: FSolidM, Scilla, Move, Obsidian, 2vyper. The comparison is fair and not self-serving.\n\nThe soft spot is exactly what the stress-test note flags. Property 1 in Section 5 is the entire bridge between Asp-level proofs and guarantees about deployed Solidity, and it is stated without proof. The corollary says 'assuming correct compilation,' but correct compilation is precisely what needs to be shown. There is no simulation relation between the cascade semantics and the EVM behavior of the compiled code, no argument that the reentrancy counter exactly enforces the R=1 recurrence limit, no treatment of how Solidity reverts align with the Asp notion of an undefined transition. The authors even acknowledge that overflow causes the compiled transaction to revert while the Asp transition is defined—so the language inclusion goes only one way, and the safety transfer has an extra edge case. That is a real gap, not a stylistic complaint.\n\nThat said, I don't think this is a hopeless paper. The proof rules for safety, reachability, and the game-style liveness property all come with soundness sketches based on standard automata and ranking arguments. The missing piece is the compiler correctness argument, and that is something the authors could provide with a more detailed operational argument or a verified artifact. The fact that the implementation is not released makes it worse, but the design is coherent enough that a serious referee could meaningfully evaluate it.\n\nThis paper is for researchers in smart contract verification who want to see a different point in the design space. I would not accept it as is, but I would send it to review and ask for proof or artifact. The gap is real but fixable.\n\nRecommendation: engage with it, but condition acceptance on a real proof of Property 1 or a released compiler.","headline":"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.","tokens_in":18431,"tokens_out":2949,"would_cite":true,"duration_ms":28886,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["Asp","smart contracts","deductive verification","defensive compilation","reentrancy","safety properties","Solidity","finite-state machines"],"falsifier":"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.","tokens_in":17424,"feed_emoji":"🔒","tokens_out":4360,"duration_ms":37815,"temperature":0.7,"pith_summary":"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.","feed_headline":"Safety proofs written once carry into deployed smart contracts","feed_subtitle":"Asp's cascade semantics blocks reentrancy and transfers safety properties to the compiled Solidity code.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"The Viper verification backend that checks the lemmas generated from Asp proof sketches.","marker":"[15]"},{"why":"The KEVM formal semantics of the EVM, which would be needed to justify the Asp-to-Solidity transfer but is not connected to the cascade semantics.","marker":"[12]"},{"why":"Source of the rank-function proof rule used for liveness and lockout-freedom.","marker":"[16]"},{"why":"The proof-carrying-code principle motivating independently checkable proofs for contract participants.","marker":"[17]"},{"why":"Defines safety and liveness, the property classes the Asp proof checker targets.","marker":"[4]"}],"fun_headline_variants":["Prove once, deploy safely: ASP's compiled contracts carry proofs","ASP: language, compiler, checker for provable safety","Reentrancy blocked by design: ASP's cascade semantics","Compile, prove, deploy: ASP secures the smart contract pipeline","Safety properties survive compilation: ASP's cascade proof"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Prove once, deploy safely: ASP's compiled contracts carry proofs","ASP: language, compiler, checker for provable safety","Reentrancy blocked by design: ASP's cascade semantics","Compile, prove, deploy: ASP secures the smart contract pipeline","Safety properties survive compilation: ASP's cascade proof"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000903,"raw_usage":{"total_tokens":3800,"prompt_tokens":773,"completion_tokens":3027,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":389,"completion_tokens_details":{"reasoning_tokens":2942}},"tokens_in":389,"tokens_out":3027,"duration_ms":19863,"temperature":1.0,"reasoning_tokens":2942,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T15:08:28.126800+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"In: VMCAI","cited_arxiv_id":null,"evidence_quote":"The Viper verification backend that checks the lemmas generated from Asp proof sketches."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The KEVM formal semantics of the EVM, which would be needed to justify the Asp-to-Solidity transfer but is not connected to the cascade semantics."},{"cited_title":"In: CA V","cited_arxiv_id":null,"evidence_quote":"Source of the rank-function proof rule used for liveness and lockout-freedom."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines safety and liveness, the property classes the Asp proof checker targets."}],"review_version":1}