Pith. sign in

REVIEW 3 major objections 4 minor 43 references

Operational Semantics for Crystality: A Smart Contract Language for Parallel EVMs

T0 review · 3 major / 4 minor · reviewed 2026-08-16 · deepseek-v4-flash

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

Pith's one-line read The first formal semantics for Crystality makes parallel-EVM contract execution machine-checkable.

desk verdict First SOS for a parallel-EVM smart contract language, but the relay semantics never executes relayed transactions, so the verified token-transfer claim is narrower than advertised. read the letter →

arxiv 2504.17336 v1 pith:MUZ7JGDM submitted 2025-04-24 cs.PL

Ziyun Xu , Hao Wang , Meng Sun This is my paper · ORCID
classification cs.PL
keywords CrystalityoperationalsemanticsparallelEVMsmartcontractsProgrammableContractScopesAsynchronousFunctionalRelayCoqformalverification
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

Crystality lets a smart contract split its state into address-, engine-, and global-scoped storage, and lets functions in one scope fire asynchronous relay calls that are packaged as transactions and shipped to other engines. The paper sets out to show that this concurrency-oriented language has a precise execution model: it gives structural operational semantics rules for declarations, assignments, function calls, relay calls, and transactions, and then encodes the rules in the Coq proof assistant. The key claim is that the semantics is faithful enough to prove real correctness properties, demonstrated by a simplified ERC20-style transfer: a transfer within balance decreases the sender's balance and adds a relay transaction crediting the payee to the payee engine's mempool, while an over-balance transfer leaves the ledger unchanged. A reader should care because, if the semantics is right, parallel-EVM smart contracts no longer have to be reasoned about informally; rule-level reasoning and machine-checked proofs become possible for exactly the features, state scoping and asynchronous relay, that make parallel execution hard.

What carries the argument

The carrier of the argument is a small-step structural operational semantics on an explicit global configuration, written as a transition $\sigma_1,\Omega_1,\mathit{Prog}_1,\dots,\sigma_n,\Omega_n,\mathit{Prog}_n,G \to \sigma'_1,\dots,G'$. Each $\sigma_i$ holds storage split into $k$ address partitions plus an engine partition, and its memory stack records the current function's scope and return slot. Two mechanisms do the conceptual work: the scope-access rules, which restrict reads and writes according to whether the current function is @address, @engine, or @global, and the relay rules, which interpret a relay statement as an immediate return plus insertion of a packaged transaction into a target engine's mempool. A named auxiliary device is the T-function: transaction execution is modeled as the outermost function call, with the memory stack cleared before and after, so transactions change storage, global storage, and mempools but not engine memory.

What would settle it

Check the machine-checked artifact at [9]: if the proof establishes that a successful transfer leads, without any further relay execution, to the payee's balance being credited, then the paper's own claim that a relay transaction is merely created is wrong. At the semantic level, a failing conformance test would be a two-engine Crystality node that accepts a @global variable update performed by only one engine, since rules SDg and IFgg require all engines to run the same global statement simultaneously.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is that Crystality's two novel constructs, Programmable Contract Scopes and Asynchronous Functional Relay, can be captured by a structural operational semantics that is precise enough to mechanize. The model is an explicit global machine: a configuration is a tuple of $n$ engines, each with storage $\sigma_i=(\Psi_i,M_i)$ (partitioned state storage plus a temporary-variable stack), a mempool $\Omega_i$ of pending relay transactions, and a program counter $\mathit{Prog}_i$, together with a single global storage $G$. The @global rules require all engines to execute identical code simultaneously, which is how global variables stay consistent; the relay rules make a relay statement return immediately while inserting a packaged transaction into the target engine's mempool. The Coq development proves, for the simplified transfer contract, that a successful transfer decrements the sender's balance and creates the relay transaction for the payee, and that a failed transfer changes nothing; the paper is explicit that this guarantee is about the relay being created, not about the payee's eventual balance.

Load-bearing premise

The rules assume every @global operation is executed at the same time by every engine on identical code, with a fixed number of engines and addresses; if a real Crystality system lets engines drift, reshard, or process global updates at different times, the semantics describes an idealized system rather than the deployed one.

Editorial extensions

If this is right

  • Because the semantics is structural, contract behavior can be reasoned about rule by rule; a developer of a parallel-EVM contract can predict exactly which engine's storage and mempool a statement touches.
  • The Coq encoding means correctness statements about Crystality contracts are machine-checkable rather than paper arguments, and the token-transfer proof is a template for similar balance invariants.
  • The relay rules make precise that a relay call is asynchronous: the caller's state changes immediately, while the recipient's credit exists only as a mempool entry until a later relay transaction runs.
  • The @global rules impose a synchronization discipline that any implementation of Crystality must respect, giving implementers a conformance target for global variables.
  • The semantics distinguishes what a transaction guarantees at commit, ledger changes plus enqueued relays, from what it does not guarantee, the eventual execution of those relays.

Reading between the lines

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

  • A natural next step the paper does not take is a confluence or commutativity theorem: proving that two relay transactions targeting different addresses produce the same final ledger regardless of order would justify the language's parallelism claim.
  • The scope-access table can be read as a static type discipline; one could build a compile-time checker that rejects writes to @global from @engine functions, preventing a class of ledger-inconsistency bugs before execution.
  • The semantics treats the engine count $n$ and addresses per engine $k$ as fixed; a testable extension is a dynamic-sharding version where $k$ or $n$ changes between transactions, which would show which guarantees survive resharding.
  • Because the verified guarantee stops at relay creation, extending the proof to eventual payee credit would require modeling mempool inclusion and relay transaction execution; the current result is narrower than a full 'transfer completes' statement.
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

3 major / 4 minor

Summary. The paper proposes a structural operational semantics for Crystality, a smart-contract language targeting parallel EVMs. It introduces a global configuration of n engines, each with storage, memory, and a mempool, plus a global storage G, and defines rules for state variable declarations, assignments, function calls, expression evaluation, relay calls, transactions, and (in the appendix) parallel and mempool behavior. The paper also reports a Coq formalization and a simplified ERC20 token-transfer case study. The advertised contributions are the first formal semantics for Crystality, including Programmable Contract Scopes and Asynchronous Functional Relay, and a machine-checked verification of a token transfer.

Significance. The paper addresses a real gap: Crystality lacks a published formal semantics, and its scoping and relay mechanisms are exactly the features that need precise formal treatment. The manuscript contains a substantial syntactic grammar, a detailed configuration model, a large set of rule schemas, and an openly referenced Coq artifact [9], and the token-transfer example is a genuine attempt at a mechanized correctness statement rather than a restatement of the rules. If the semantics were made complete and well-formed, and the Coq development fully presented, this would be a useful foundation for verifying parallel-EVM smart contracts. At present, however, the relay gap and the malformed rules prevent the stated claims from being verified from this text.

major comments (3)
  1. [§3.2, RELa/RELs/RELg1/RELg2; Appendix A MemP/Para] The relay rules only package a call into a relay transaction and add it to a mempool; no rule consumes a transaction from any Ω and begins executing the relayed function. The transaction rules IFta/IFts/IFtg and EFta/EFts/EFtg in Appendix C are triggered by an explicit function call in Prog_i, and membership of a relay transaction in Ω_i has no derivation that turns it into such a call. MemP in Appendix A is, at best, a commutation condition on mempool differences and does not model consumption. Consequently, a relayed mint can never execute in the semantics, the recipient's balance cannot increase, and the §4 claim that the relay transaction is created 'to increase the recipient's balance' is not a derivable property. This gap is internal to the formalization, not an external idealization, because asynchronous execution of relayed calls is the defining feature the paper claims to formalize.
  2. [Appendix A, Para and MemP; also SDg and TAg] Para and MemP are not well-formed inference rules: Para consists of one equation and three transition-like expressions with no unambiguous premise/conclusion separation, and MemP has an equation and two transition-like expressions that cannot be read as a standard rule. The SDg rule contains the malformed notation '[NG′(id)size(T ype) G′]', and the TAg rule has a conclusion involving σ′i and M′i that are not determined by its premises. Because these are the only formal rules covering parallel execution, global synchronization, and mempool behavior, the corresponding parts of the claimed semantics are not currently defined.
  3. [§4, last paragraph] The text explicitly states that the full Coq formalization and verification are not provided in the paper and are 'available at [9]', and that the current formalization does not yet account for 'the semantics of parallelism and synchronization'. This admission is in tension with the abstract's claim that the syntax and semantics are mechanized in Coq and leaves the mechanization claim unverifiable from the manuscript; at minimum, the paper must state exactly which rules are encoded and which are excluded, and should include the Coq development or a precise theory listing.
minor comments (4)
  1. [References] Reference [9] is listed as only a DOI with no title, authors, or description; it should be a full citation to the artifact, and the artifact should be linked in the paper.
  2. [§3.1] The text 'Λ body : IDF → Prog givens the function body' contains a typo ('givens' for 'gives'); the paper also uses 'P rog' and 'T able' with spurious spaces in several places, presumably from LaTeX line breaking, which should be cleaned up in the camera-ready version.
  3. [§2.3] The EBNF defines '⟨stmt⟩ ::= ⟨pstmt⟩ | ⟨stmt⟩ ⟨stmt⟩' without an explicit separator, making the sequencing rule ambiguous; please add an explicit separator or a note that whitespace is the separator.
  4. [§3.2 and Appendix A] The paper promises that 'the formal rules for other function calls are omitted here but are fully detailed in the appendix,' yet the appendix contains only IFaa, IFas, IFss, and IFgg; please state explicitly which scope combinations are legal and why the remaining combinations are absent.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity: the SOS rules are self-contained definitions, not restatements of their own conclusions; the only self-citation (Crystality's origin paper [39]) is not load-bearing.

full rationale

The paper's derivation chain is a definitional semantics: its inputs are the syntax of Crystality and the informal scope/relay design from the prior Crystality paper [39], and its outputs are structural operational rules plus a Coq-verified token-transfer theorem. There is no fitted parameter renamed as a prediction; the token-transfer theorem states that under the defined rules the sender balance decreases and a relay transaction is added to the recipient engine's mempool, which is a genuine consequence of rules IFta/SAaa/RELa rather than an axiom or restatement. The relation to [39] is a self-citation (author Hao Wang overlaps), but it is context-setting: the semantics is stated in full in Sections 3 and Appendices A-C, and the correctness claim is about those stated rules, not about an unverified uniqueness theorem or imported ansatz. The paper's own limitation statement in Section 4 concedes that the semantics of parallelism and synchronization are not fully captured, and the reviewer-visible gap that relayed transactions are never executed by any rule is a semantic incompleteness/correctness limitation, not a circular reduction: the paper does not claim the relayed mint runs within the same derivation step, and the verified statement is about mempool insertion. Thus no circular step is exhibited; score 2 reflects only the minor, non-load-bearing self-citation of the language's origin.

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

The central claim rests on the correctness and completeness of the prior Crystality language definition, on standard map abstractions for storage, and on two idealizations: lockstep global execution and asynchronous relay that only touches mempools. No free parameters are fitted to data. No new entities are introduced beyond modeling devices.

assumptions (4)
  • domain assumption The informal Crystality specification in Wang et al. [39] is complete enough to formalize.
    The semantics is written for a language defined in the authors' earlier PPoPP paper; there is no independent formal specification to check against.
  • standard math Storage and memory are modeled as maps A to B with associated name spaces and type spaces, and functions allocate_new, init, and size are well-defined.
    Section 3.1 introduces these notations but does not define the map operations; they are assumed background.
  • domain assumption All @global operations are executed by every engine simultaneously on identical code, and the system has a fixed number n of engines and k addresses per engine.
    Rules SDg, IFgg, IFtg, TAg, and SAgg all require identical code across all engines in one transition; this lockstep model is an idealization of real asynchronous blockchains.
  • domain assumption Relay calls are asynchronous: they only add entries to mempools and do not affect execution of the current transaction.
    Rules RELa, RELs, RELg1, RELg2 and MemP model relay as mempool insertion, while transaction execution is isolated from the mempool; eventual execution of relay transactions is not modeled.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Operational Semantics for Crystality: A Smart Contract Language for Parallel EVMs." pith.science (2026). https://pith.science/paper/MUZ7JGDM

@misc{pith2026250417336,
  author       = {Pith},
  title        = {Pith review of: Operational Semantics for Crystality: A Smart Contract Language for Parallel EVMs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/MUZ7JGDM}},
  note         = {Machine review of arXiv:2504.17336}
}
read the original abstract

The increasing demand for scalable blockchain has driven research into parallel execution models for smart contracts. Crystality is a novel smart contract programming language designed for parallel Ethereum Virtual Machines (EVMs), enabling fine-grained concurrency through Programmable Contract Scopes and Asynchronous Functional Relay. This paper presents the first formal structural operational semantics for Crystality, providing a rigorous framework to reason about its execution. We mechanize the syntax and semantics of Crystality in the theorem-proving assistant Coq, enabling formal verification of correctness properties. As a case study, we verify a simplified token transfer function, demonstrating the applicability of our semantics in ensuring smart contract correctness. Our work lays the foundation for formally verified parallel smart contracts, contributing to the security and scalability of blockchain systems.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

43 extracted references · 37 canonical work pages

  1. [9]

    (2025), https://doi.org/10.5281/zenodo.14991761

    work page doi:10.5281/zenodo.14991761 2025

  2. [1]

    Solidity airdrop smart contract (2018), https://github.com/SpringRole/smart-contracts/blob/master/contracts

    work page 2018

  3. [2]

    8 innovations that make solana the first web-scale blockch ain (2019), https://solana.com/news/8-innovations-that-make-sol ana-the-first-web-scale-blockchain

    work page 2019

  4. [3]

    Solidity documentation (2021), https://docs.soliditylang.org/en/latest/

    work page 2021

  5. [4]

    The aptos blockchain: safe, scalable, and upgradeable we b3 infrastructure (2022), https://aptosfoundation.org/whitepaper/aptos-whitepaper_en.pdf

    work page 2022

  6. [5]

    Sei: The layer 1 for trading (2023), https://github.com/sei-protocol/sei-chain/blob/main/whitepaper/Sei_Whi

    work page 2023

  7. [6]

    Solidity by example: Voting (2023), https://docs.soliditylang.org/en/v0.8.21/solidity-by-example.html

    work page 2023

  8. [7]

    The sui smart contracts platform (2023), https://docs.sui.io/paper/sui.pdf

    work page 2023

Show all 43 references
  1. [8]

    The monad white paper (2024), https://files.monadpad.xyz/whitepaper.pdf

    2024

  2. [10]

    In: Theorem Proving in Higher Order Logics : 16th International Conference, TPHOLs 2003, Rome, Italy, September 8-12, 2003

    Andronick, J., Chetali, B., Ly, O.: Using coq to verify ja va card tm applet isola- tion properties. In: Theorem Proving in Higher Order Logics : 16th International Conference, TPHOLs 2003, Rome, Italy, September 8-12, 2003 . Proceedings 16. pp. 335–351. Springer (2003)

    2003

  3. [11]

    In : 2019 27th Euromicro International Conference on Parallel, Distributed and Net work-Based Processing (PDP)

    Anjana, P.S., Kumari, S., Peri, S., Rathor, S., Somani, A .: An efficient framework for optimistic concurrent execution of smart contracts. In : 2019 27th Euromicro International Conference on Parallel, Distributed and Net work-Based Processing (PDP). pp. 83–92. IEEE (2019)

    2019

  4. [12]

    Springe r Science & Business Me- dia (2013)

    Bertot, Y., Castéran, P.: Interactive theorem proving a nd program development: Coq’Art: the calculus of inductive constructions. Springe r Science & Business Me- dia (2013)

    2013

  5. [13]

    move: A language with programmable resources (2020)

    Blackshear, S., Cheng, E., Dill, D.L., Gao, V., Maurer, B ., Nowacki, T., Pott, A., Qadeer, S.: Rain, dario russi, stephane sezer, tim zakian, a nd runtian zhou. move: A language with programmable resources (2020)

    2020

  6. [14]

    In: Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Princi ples

    Chen, Y., Guo, Z., Li, R., Chen, S., Zhou, L., Zhou, Y., Zha ng, X.: Forerunner: Constraint-based speculative transaction execution for e thereum. In: Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Princi ples. pp. 570– 587 (2021)

    2021

  7. [15]

    In: Proceed- ings of the 18th ACM SIGPLAN international conference on Fun ctional program- ming

    Chlipala, A.: The bedrock structured programming syste m: Combining generative metaprogramming and hoare logic in an extensible program ve rifier. In: Proceed- ings of the 18th ACM SIGPLAN international conference on Fun ctional program- ming. pp. 391–402 (2013)

    2013

  8. [16]

    V ALID pp

    Crosara, M., Centurino, G., Arceri, V.: Towards an opera tional semantics for so- lidity. V ALID pp. 1–6 (2019)

    2019

  9. [17]

    In: Unifying Theories of Programming: 5th Inter national Symposium, UTP 2014, Singapore, May 13, 2014, Revised Selected Papers 5

    Foster, S., Zeyda, F., Woodcock, J.: Isabelle/utp: A mec hanised theory engineering framework. In: Unifying Theories of Programming: 5th Inter national Symposium, UTP 2014, Singapore, May 13, 2014, Revised Selected Papers 5 . pp. 21–41. Springer (2015)

    2015

  10. [18]

    In: Proceedings of the 44th International Conference on Sof tware Engineering

    Garamvölgyi, P., Liu, Y., Zhou, D., Long, F., Wu, M.: Util izing parallelism in smart contracts on decentralized blockchains by taming applicat ion-inherent conflicts. In: Proceedings of the 44th International Conference on Sof tware Engineering. pp. 2315–2326 (2022)

    2022

  11. [19]

    In: Proceedings of the 28th ACM SIGPL AN Annual Sym- posium on Principles and Practice of Parallel Programming

    Gelashvili, R., Spiegelman, A., Xiang, Z., Danezis, G., Li, Z., Malkhi, D., Xia, Y., Zhou, R.: Block-stm: Scaling blockchain execution by turni ng ordering curse to a performance blessing. In: Proceedings of the 28th ACM SIGPL AN Annual Sym- posium on Principles and Practice o...

    2023

  12. [20]

    IACR Cryptol

    Georgiadis, E.: How many transactions per second can bit coin really handle? the- oretically. IACR Cryptol. ePrint Arch. p. 416 (2019)

    2019

  13. [21]

    In: Verified Software

    Hajdu, Á., Jovanovic, D.: solc-verify: A modular verifie r for solidity smart con- tracts. In: Verified Software. Theories, Tools, and Experim ents. LNCS, vol. 12031, pp. 161–179. Springer (2019)

    2019

  14. [22]

    In: Proceedings of ESOP 2020

    Hajdu, Á., Jovanovic, D.: Smt-friendly formalization o f the solidity memory model. In: Proceedings of ESOP 2020. LNCS, vol. 12075, pp. 224–250. Springer (2020)

    2020

  15. [23]

    In: Proceedings of the 1 3th ACM SIGPLAN Symposium on Principles and practice of parallel programmi ng

    Herlihy, M., Koskinen, E.: Transactional boosting: a me thodology for highly- concurrent transactional objects. In: Proceedings of the 1 3th ACM SIGPLAN Symposium on Principles and practice of parallel programmi ng. pp. 207–216 (2008)

    2008

  16. [24]

    In: Proceedings of CSF 2018

    Hildenbrandt, E., Saxena, M., Rodrigues, N., Zhu, X., Da ian, P., Guth, D., Moore, B.M., Park, D., Zhang, Y., Stefanescu, A., Rosu, G.: KEVM: A c omplete formal semantics of the ethereum virtual machine. In: Proceedings of CSF 2018. pp. 204–

    2018

  17. [25]

    Prentice Hall (1998)

    Hoare, C.A.R., He, J.: Unifying theories of programming . Prentice Hall (1998)

    1998

  18. [26]

    Rap- port Technique 178, 113 (1997)

    Huet, G., Kahn, G., Paulin-Mohring, C.: The coq proof ass istant a tutorial. Rap- port Technique 178, 113 (1997)

    1997

  19. [27]

    CoRR abs/1804.01295 (2018), http://arxiv.org/abs/1804.01295

    Jiao, J., Kan, S., Lin, S., Sanán, D., Liu, Y., Sun, J.: Exe cutable operational semantics of solidity. CoRR abs/1804.01295 (2018), http://arxiv.org/abs/1804.01295

    2018 arXiv

  20. [28]

    In: Proceedings of SP 2020

    Jiao, J., Kan, S., Lin, S., Sanán, D., Liu, Y., Sun, J.: Sem antic understanding of smart contracts: Executable operational semantics of soli dity. In: Proceedings of SP 2020. pp. 1695–1712. IEEE (2020)

    2020

  21. [29]

    In: Interactive Theorem Proving: 5th International C onference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, A ustria, July 14-17, 2014

    Krebbers, R., Leroy, X., Wiedijk, F.: Formal c semantics : Compcert and the c stan- dard. In: Interactive Theorem Proving: 5th International C onference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, A ustria, July 14-17, 2014. Proceedings 5. pp. 543–...

    2014

  22. [30]

    ACM Transactions on Database Systems (TODS) 6(2), 213–226 (1981)

    Kung, H.T., Robinson, J.T.: On optimistic methods for co ncurrency control. ACM Transactions on Database Systems (TODS) 6(2), 213–226 (1981)

    1981

  23. [31]

    In: Proceedings of SEFM 2021

    Marmsoler, D., Brucker, A.D.: A denotational semantics of solidity in isabelle/hol. In: Proceedings of SEFM 2021. LNCS, vol. 13085, pp. 403–422. Springer (2021)

    2021

  24. [32]

    Nakamoto, S.: Bitcoin: A peer-to-peer electronic cash s ystem (2008), https://bitcoin.org/bitcoin.pdf

    2008

  25. [33]

    In: International Conference on Automated Deduction

    Owre, S., Rushby, J.M., Shankar, N.: Pvs: A prototype ver ification system. In: International Conference on Automated Deduction. pp. 748– 752. Springer (1992)

    1992

  26. [34]

    Plotkin, G.D.: A structural approach to operational sem antics (1981)

    1981

  27. [35]

    In: 2023 IEEE 43rd International Conference on Di stributed Computing Systems (ICDCS)

    Qi, X., Jiao, J., Li, Y.: Smart contract parallel executi on with fine-grained state accesses. In: 2023 IEEE 43rd International Conference on Di stributed Computing Systems (ICDCS). pp. 841–852. IEEE (2023)

    2023

  28. [36]

    Sanka, A.I., Cheung, R.C.C.: A systematic review of bloc kchain scalability: Issues, solutions, analysis and future research. J. Netw. Comput. A ppl. 195, 103232 (2021)

    2021

  29. [37]

    arXiv preprint arXiv:1901.01376 (2019)

    Saraph, V., Herlihy, M.: An empirical study of speculati ve concurrency in ethereum smart contracts. arXiv preprint arXiv:1901.01376 (2019)

    2019 arXiv

  30. [38]

    In: Inte rnational Conference on Theorem Proving in Higher Order Logics

    Slind, K., Norrish, M.: A brief overview of hol4. In: Inte rnational Conference on Theorem Proving in Higher Order Logics. pp. 28–32. Springer (2008)

    2008

  31. [39]

    In: Proceedings of the 30th ACM SIGP LAN Annual Symposium on Principles and Practice of Parallel Programmi ng

    Wang, H., Pan, M., Wang, J.: Crystality: A programming mo del for smart con- tracts on parallel evms. In: Proceedings of the 30th ACM SIGP LAN Annual Symposium on Principles and Practice of Parallel Programmi ng. p. 412–425. PPoPP ’25, Association for Computing Machinery, New ...

    2025

  32. [40]

    MIT Press (1993)

    Winskel, G.: The formal semantics of programming langua ges - an introduction. MIT Press (1993)

    1993

  33. [41]

    CoRR abs/1803.09885 (2018), http://arxiv.org/abs/1803.09885

    Yang, Z., Lei, H.: Lolisa: Formal syntax and semantics fo r a sub- set of the solidity programming language. CoRR abs/1803.09885 (2018), http://arxiv.org/abs/1803.09885

    2018 arXiv

  34. [42]

    In: Verified Software

    Zakrzewski, J.: Towards verification of ethereum smart c ontracts: A formalization of core of solidity. In: Verified Software. Theories, Tools, and Experiments. LNCS, vol. 11294, pp. 229–247. Springer (2018) A Semantic Rules of Statements MemP Ω ′ i \ Ω i = ¯Ω i \ ˆΩ i (σ1, Ω 1,...

    2018

  35. [217]

    IEEE Computer Society (2018)

    2018

Pith tools

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