Pith. sign in

REVIEW 5 major objections 5 minor 40 references

Legal Compliance Evaluation of Smart Contracts Generated By Large Language Models

T0 review · 5 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Pith's one-line read This paper tries to establish that the legal compliance of smart contracts generated by large language models can be quantified by modeling both the legal contract and the generated code as Petri nets and measuring behavioral conformance…

desk verdict Useful empirical comparison of LLMs on smart contract generation, but the compliance metrics are repackaged conformance checking and the hand-built ground truth is too subjective to support the central claim. read the letter →

arxiv 2506.00943 v1 pith:QU3ZSEKQ submitted 2025-06-01 cs.SE cs.AI

classification cs.SEcs.AI
keywords largelanguagemodelssmartcontractslegalcompliancePetrinetsreachabilityanalysissoftwaremetricsSoliditybehavioralequivalence
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

Smart contracts produced by large language models can be syntactically valid yet legally incomplete, and this paper's project is to make that gap measurable. It models a natural-language legal contract and each LLM-generated Solidity contract as a Petri net, then compares the sets of behaviors reachable in the two nets. Three metrics—fitness (how many legal behaviors the code contains), precision (how much extra behavior the code adds), and a functional equivalence score—turn the comparison into numbers. Applied to twenty smart contracts from four LLMs over five legal contracts, the method finds large variance, with larger models generally closer to the legal ground truth and the best model reaching a fitness of 0.5 on the most complex contract while the others scored 0. The authors conclude that LLMs can assist in producing starter code for legally compliant smart contracts under strict review, and that this metric suite can support automated, self-improving development workflows.

What carries the argument

The machinery is a Petri net model of each contract, with places standing for legal positions (powers and obligations) and transitions standing for actions or events; the reachability graph of the net enumerates the contract's possible behaviors. Legal positions are derived from a formal legal-contract ontology, and comparison requires legal equivalence of ending states. A loop-control place with an inhibitor arc stops self-looping transitions from firing repeatedly, keeping the graph finite. The metric formulas themselves carry the argument: they map behavior-set overlap onto compliance scores, with fitness $F(SC,LC)=|R\cap Q|/|R|$, precision $Pr(SC,LC)=|(R\cap Q)^*|/|Q|$, and functional equivalence score $FES(SC,LC)=|(R\cap Q)^*|/|R|$.

What would settle it

Take a contract that a panel of lawyers agrees a smart contract implements completely and correctly; if the pipeline gives that contract a fitness or functional equivalence score below 1, the nets or metrics are missing compliant behavior. A second check: have two independent teams build legal Petri nets from the same contract; if their metric rankings differ, manual modeling choices rather than the contract's content are driving the scores.

Watch

Extended reading notes

Core claim

The central claim is that legal compliance can be treated as behavioral conformance: a smart contract complies to the degree that the reachable behaviors of its process model match the reachable behaviors of the legal contract's process model. The paper formalizes this with fitness $F(SC,LC)=|R\cap Q|/|R|$, precision $Pr(SC,LC)=|(R\cap Q)^*|/|Q|$, and functional equivalence score $FES(SC,LC)=|(R\cap Q)^*|/|R|$, where $R$ and $Q$ are the legal and smart-contract behavior sets. It applies these metrics to 20 smart contracts generated by four LLMs from five legal contracts and reports that all outputs compile but compliance varies widely; the absence of administrative powers such as pausing is a recurring reason for zero scores. The paper also argues the metrics satisfy standard measurement properties, giving them a ratio scale and making them usable for comparing models and for feeding an automated, self-improving development loop.

Load-bearing premise

The load-bearing premise is that the manually built Petri nets accurately and completely capture every legally relevant behavior of both the legal text and the generated code; if a model omits or distorts a workflow, every compliance score inherits that error.

Editorial extensions

If this is right

  • Compliance becomes a number: LLM outputs can be ranked by fitness, precision, and functional equivalence instead of being judged only by whether they compile.
  • The same metrics can judge manually written smart contracts, since the process-model comparison does not depend on how the code was produced.
  • An automated loop becomes plausible: a generated contract's score can be fed back as a signal for iterative improvement of prompts or models.
  • Complex contracts with many legal positions can produce combinatorial path explosion, so scaling the method calls for cheaper graph-comparison techniques.

Reading between the lines

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

  • Because the metrics only need a ground-truth behavior set, a statute or regulation could replace the bilateral legal contract, making the method a template for automated regulatory compliance scoring; the paper does not pursue this.
  • The recurring zero scores for missing administrative functionality such as pausing suggest that safeguards, not core business logic, are the main compliance bottleneck, a pattern that could guide targeted prompt engineering.
  • Precision and fitness trade off in the reported results much like under- and over-approximation in formal verification, so a combined compliance region rather than a single threshold may be the natural way to read the scores.
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

5 major / 5 minor

Summary. The paper proposes a metric suite (fitness, precision, functional equivalence score) for quantifying the legal compliance of smart contracts generated by LLMs. The approach models both the natural-language legal contract and the smart contract as Petri nets, derives their reachability graphs, and compares behaviors under strict and non-strict event equivalence. The authors apply the suite to 20 smart contracts generated by four LLMs (GPT-4o, Gemini 1.5 Pro, Claude 3.5 Sonnet, Llama 3.1 70b) from five legal contracts, reporting that while all models produce syntactically valid code, their legal compliance varies, with larger models generally performing better. They also evaluate the metrics against properties of software measures and discuss threats to validity.

Significance. The idea of using process-model conformance to evaluate legal compliance is novel and potentially useful for automating smart-contract quality assessment. The paper is transparent about its modeling choices and provides artifacts online. However, the central validity question is not resolved: the metrics compare two hand-built Petri nets, and the ground-truth legal PNs involve deliberate simplifications (e.g., omitting workflows, exempting temporal events) that can change the ranking of LLMs. Without validation against an external gold standard or a formal account of state equivalence, the claim that the metrics quantify legal compliance remains unsupported. If the authors can address these concerns, the paper would make a solid contribution.

major comments (5)
  1. [Sec. III-A (legal PN construction)] The ground-truth legal Petri nets are constructed manually and include deliberate omissions: the text states that "blacklisting, freezing, and terminating accounts lead to similar outcomes. Thus, blacklisting is selected as the representative workflow excluding others." Since the legal PN defines the behavior set R used in Eqs. (1)-(3), omitting these workflows changes both the denominator |R| and the intersections |R∩Q|. The reported GCDC results (Table IV: Claude 3.5 Sonnet fitness 0.5, all other models 0) are a direct consequence of this choice: the legal reachability graph ends every path with the "pause" transition, so any implementation lacking pause (e.g., GPT-4o, which implements freezing but not pausing) receives zero. If freezing or termination had been modeled as separate powers, the legal behavior set would include additional paths, and the relative ranking of the models could change. The paper provides no justification that the omitted workflows are legally equivalent to blacklisting, and no sensitivity analysis to show the results are robust to this modeling decision.
  2. [Sec. II-C and Sec. IV-A] The treatment of temporal events is underspecified. Section II-C establishes the exemption for "the passing of time, such as deadline expiry" from strict event equivalence, and Section IV-A states that temporal events "may be realized without any code execution." However, the paper does not define what constitutes a "legally equivalent state" when a temporal event is absent from the candidate reachability graph. For example, if a legal contract states that a power expires at a deadline, a smart contract that does not enforce this expiration may still hold the token in the corresponding place, and the final marking would not be legally equivalent. Without a formal and operational definition of state equivalence under temporal exemptions, the fitness and FES values may overstate compliance. This is load-bearing because the exemption is used in the computation of the metrics.
  3. [Sec. IV, Eqs. (1)-(3)] The metric definitions are not sufficiently precise to be reproducible. The sets R and Q are described as behavior sets (paths in reachability graphs), but the paper does not provide an algorithm for computing |R∩Q| and |(R∩Q)*| under the strict and non-strict event-equivalence relations. The statement in Sec. IV-A that "when multiple behaviors in a smart contract map to a behavior in the legal contract, they are counted as one" is ambiguous for counting the numerator of precision, where a single legal behavior may partially match several candidate behaviors. This ambiguity affects the reported numbers in Table IV and undermines the claim in Sec. VI-B that the metrics have a ratio scale.
  4. [Sec. V-B-3 and Table IV] The treatment of the Transactive Energy contract undermines the claimed general applicability of the metrics. The paper reports a "path explosion problem" and states that the analysis was "optimized by identifying subsequences of events with clear legality violations and discounting them from metric calculations." This ad-hoc discounting is not described formally, and the precision value for this contract is missing (shown as ✗ in Table IV). As a result, the metric suite cannot currently handle one of the five contracts, contradicting the statement in the abstract and Sec. IV that the metrics are "applicable across domains." A complete algorithmic account of how to handle large reachability graphs, or a clear scope restriction, is required.
  5. [Sec. VI-C (Construct validity)] The paper acknowledges that "some legal nuances might still be lost in the translation to PN representations." Since the legal PN is the ground truth and is built by the authors from the legal text, and the smart-contract PN is also built by the authors from the code, the metrics compare two models produced by the same modeling process. The inclusion of two lawyers in the loop reduces, but does not eliminate, the risk of systematic modeling bias. No external validation is provided: the metrics are not compared against human expert assessments of compliance or against any independent formal specification. Consequently, the central claim that fitness, precision, and FES quantify legal compliance is not yet supported. The authors should validate the metrics against an external gold standard or at least demonstrate robustness of the ranking to alternative model constructions.
minor comments (5)
  1. [Sec. I] The text contains a doubled comma: "However,," should be "However,".
  2. [Table III] The table header "Large ANGUAGE MODELS" is misspelled; it should read "LANGUAGE".
  3. [Sec. IV-B] The notation "(R∩Q)*" is used without an explicit definition; please explain how non-strict matching is applied in the counting process.
  4. [Sec. VI-B] The claim that all three metrics have a "ratio scale" is asserted without justification; please provide a measurement-theoretic argument or qualify the claim.
  5. [Sec. III-A-2] The introduction of loop-control places prevents repeated firings of transitions; since legal contracts may permit repeated actions (e.g., multiple payments), please justify this simplification or analyze its effect on the computed metrics.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the compliance metrics are explicit set-overlap ratios over independently constructed Petri-net models; the acknowledged interpretation dependence is a construct-validity threat, not a circular step.

full rationale

The derivation chain is linear: legal contracts are manually modeled as Petri nets (ground-truth set R, with lawyer validation), LLM-generated smart contracts are separately modeled as Petri nets (set Q), and Eqs. (1)-(3) compute recall/precision-style ratios |R∩Q|/|R|, |(R∩Q)*|/|Q|, and |(R∩Q)*|/|R|. The legal PNs are built from the legal text and do not depend on the LLM outputs, so the compliance scores are not fitted to the predicted values. The paper explicitly acknowledges the fitness/recall analogy, and no load-bearing self-citation occurs (the Symboleo references are by other authors). The genuine limitation is construct validity, stated in Sec. VI-C: 'The accuracy of the proposed metrics depends on the correct interpretation of legal text' and 'Some legal nuances might still be lost in the translation to PN representations,' plus the explicit scoping in Sec. III-A: 'We do not include behaviors that may be implied beyond the explicit functional scope' and the representative-workflow choice that omits freezing and termination. These modeling assumptions could change scores, but they are inputs to a proposed operationalization, not a circular reduction: different assumptions would yield different measurements, not a result forced by the equations to equal its own input. The ad-hoc discounting of illegal subsequences in the Transactive Energy analysis is a computational deviation from the stated formulas, but it does not make the headline claim definitionally equivalent to its inputs. Hence no circular step is established.

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

The central claim rests on the manual construction of Petri nets from both legal and smart contracts. There are no numeric free parameters, but the modeling choices (omitted workflows, loop-control places, temporal exemption) are hidden assumptions that effectively act as free parameters. The absence of an independent ground truth makes the validity of the metric suite untested.

assumptions (5)
  • domain assumption The hand-built Petri net of each legal contract is a faithful and complete representation of the legally relevant behaviors of that contract, and is a suitable ground truth.
    Sec. III-A1: analysts and two lawyers manually constructed PNs from natural-language contracts; discrepancies resolved by discussion. If this interpretation is wrong, all metrics are compromised.
  • domain assumption The four-step manual transformation of smart contract Solidity code to a Petri net preserves all behaviors relevant to legal compliance.
    Sec. III-A2: the transformation is done by examining control flow and variable changes; no automated tool or formal proof is used, so fidelity depends on the analyst's judgment.
  • ad hoc to paper Basic Petri nets without token differentiation and with loop-control places still capture contract behavior well enough for compliance comparison.
    Sec. II-B and III-A2: the limitation to single instances and the addition of loop-control places restrict self-loops, which may remove legitimate repeated behaviors (e.g., repeated exercise of a power).
  • ad hoc to paper Temporal events (e.g., deadline expiry) can be exempted from strict event equivalence without affecting compliance assessment.
    Sec. IV-A: the paper exempts temporal events because they can happen without code execution, but this could hide missing deadline logic in the smart contract.
  • domain assumption Legal compliance can be operationalized as equivalence of reachable states and event sequences in Petri net models of the two contracts.
    Sec. IV: the entire metric suite assumes behavioral conformance is a valid proxy for legal compliance, which is a strong legal-semantic claim.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Legal Compliance Evaluation of Smart Contracts Generated By Large Language Models." pith.science (2026). https://pith.science/paper/QU3ZSEKQ

@misc{pith2026250600943,
  author       = {Pith},
  title        = {Pith review of: Legal Compliance Evaluation of Smart Contracts Generated By Large Language Models},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QU3ZSEKQ}},
  note         = {Machine review of arXiv:2506.00943}
}
read the original abstract

Smart contracts can implement and automate parts of legal contracts, but ensuring their legal compliance remains challenging. Existing approaches such as formal specification, verification, and model-based development require expertise in both legal and software development domains, as well as extensive manual effort. Given the recent advances of Large Language Models (LLMs) in code generation, we investigate their ability to generate legally compliant smart contracts directly from natural language legal contracts, addressing these challenges. We propose a novel suite of metrics to quantify legal compliance based on modeling both legal and smart contracts as processes and comparing their behaviors. We select four LLMs, generate 20 smart contracts based on five legal contracts, and analyze their legal compliance. We find that while all LLMs generate syntactically correct code, there is significant variance in their legal compliance with larger models generally showing higher levels of compliance. We also evaluate the proposed metrics against properties of software metrics, showing they provide fine-grained distinctions, enable nuanced comparisons, and are applicable across domains for code from any source, LLM or developer. Our results suggest that LLMs can assist in generating starter code for legally compliant smart contracts with strict reviews, and the proposed metrics provide a foundation for automated and self-improving development workflows.

Figures

Figures reproduced from arXiv: 2506.00943 by the authors.

Figure 1
Figure 1. Workflow of Petri-net-based legal and smart contract behavior analysis. [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Excerpt from the GCDC ToS contract, adapted from [ [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Petri net and reachability graph of the GCDC Terms of Service. [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Possible behaviors of a legal contract and its smart contract. [PITH_FULL_IMAGE:figures/full_fig_p004_4.png]
Figure 5
Figure 5. Figure 5: LLM Prompts for Smart Contract Generation [PITH_FULL_IMAGE:figures/full_fig_p006_5.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

40 extracted references · 37 canonical work pages

  1. [1]

    Blockchains for business process management – Challenges and opportunities,

    J. Mendlinget al., “Blockchains for business process management – Challenges and opportunities,”ACM Trans. on Management Information Systems (TMIS), vol. 9, pp. 4:1–4:16, Feb. 2018

  2. [2]

    Verisolid: Correct-by-design smart contracts for Ethereum,

    A. Mavridou, A. Laszka, E. Stachtiari, and A. Dubey, “Verisolid: Correct-by-design smart contracts for Ethereum,” inFinancial Cryp- tography and Data Security(I. Goldberg and T. Moore, eds.), (Cham), pp. 446–465, Springer Inte. Publishing, 2019

  3. [3]

    Relevance of on-chain asset tokenization in “Crypto Winter

    S. Kumar, R. Suresh, D. Liu, B. Kronfellner, and A. Kaul, “Relevance of on-chain asset tokenization in “Crypto Winter”,”Boston Consulting Group, 2022

  4. [4]

    A legal-relationship establishment in smart contracts: Ontological semantics for programming-language develop- ment,

    V . Dwivedi and A. Norta, “A legal-relationship establishment in smart contracts: Ontological semantics for programming-language develop- ment,” inAdvances in Computing and Data Sciences(M. Singh, V . Tyagi, P. K. Gupta, J. Flusser, T. ¨Oren, and V . R. Sonawane, eds.), pp. 660–676, Springer Int. Publishing, 2021

  5. [5]

    Evaluation of logic-based smart contracts for blockchain systems,

    F. Idelberger, G. Governatori, R. Riveret, and G. Sartor, “Evaluation of logic-based smart contracts for blockchain systems,” inRule Tech- nologies. Research, Tools, and Applications(J. J. Alferes, L. Bertossi, G. Governatori, P. Fodor, and D. Roman, eds.), pp. 167–183, Springer Int. Publishing, 2016

  6. [6]

    Embedded supervision: How to build regulation into blockchain finance,

    R. Auer, “Embedded supervision: How to build regulation into blockchain finance,”Globalization and Monetary Policy Institute Work- ing Paper, no. 371, 2019

  7. [7]

    Program synthesis with large language models,

    J. Austinet al., “Program synthesis with large language models,” 2021

  8. [8]

    Evaluating large language models trained on code,

    M. Chenet al., “Evaluating large language models trained on code,” 2021

Show all 40 references
  1. [9]

    Is your code generated by chatgpt really correct? Rigorous evaluation of large language models for code generation,

    J. Liu, C. S. Xia, Y . Wang, and L. Zhang, “Is your code generated by chatgpt really correct? Rigorous evaluation of large language models for code generation,” inAdvances in Neural Information Processing Systems (A. Oh, T. Naumann, A. Globerson, K. Saenko, M. Hardt, and S. Le...

  2. [10]

    Legalbench: A collaboratively built benchmark for measuring legal reasoning in large language models,

    N. Guhaet al., “Legalbench: A collaboratively built benchmark for measuring legal reasoning in large language models,” 2023

  3. [11]

    A complexity measure,

    T. J. McCabe, “A complexity measure,”IEEE Trans. on Software Engineering, vol. SE-2, no. 4, pp. 308–320, 1976

  4. [12]

    Modelling legal contracts as processes,

    A. Daskalopulu, “Modelling legal contracts as processes,” inProc. 11th Int. Workshop on Database and Expert Systems Applications, pp. 1074– 1079, IEEE, 2000

  5. [13]

    Petri Net,

    C. Petri and W. Reisig, “Petri Net,”Scholarpedia, vol. 3, no. 4, p. 6477, 2008

  6. [14]

    Fundamental legal conceptions as applied in judicial reasoning,

    W. N. Hohfeld, “Fundamental legal conceptions as applied in judicial reasoning,”The Yale Law J., vol. 26, no. 8, pp. 710–770, 1917

  7. [15]

    Parvizimosaed,Symboleo: Specification and verification of legal contracts

    A. Parvizimosaed,Symboleo: Specification and verification of legal contracts. PhD thesis, University of Ottawa, 2022

  8. [16]

    From Petri NETS to Colored Petri NETS: A tutorial introduction to NETS based formalism for modeling and simulation,

    V . Gehlot, “From Petri NETS to Colored Petri NETS: A tutorial introduction to NETS based formalism for modeling and simulation,” in2019 Winter Simulation Conf. (WSC), pp. 1519–1533, 2019

  9. [17]

    Modelling inter-organizational trade using documentary Petri nets,

    R. W. Bons, R. M. Lee, R. W. Wagenaar, and C. D. Wrigley, “Modelling inter-organizational trade using documentary Petri nets,” inProceedings of the Twenty-eighth Annual Hawaii Int. Conf. on System Sciences, vol. 3, pp. 189–198, IEEE, 1995

  10. [18]

    Formal analysis of smart contract based on colored Petri nets,

    W. Duo, H. Xin, and M. Xiaofeng, “Formal analysis of smart contract based on colored Petri nets,”IEEE Intelligent Systems, vol. 35, no. 3, pp. 19–30, 2020

  11. [19]

    CPN/Tools: A tool for editing and simulat- ing coloured Petri Nets ETAPS tool demonstration related to TACAS,

    M. Beaudouin-Lafonet al., “CPN/Tools: A tool for editing and simulat- ing coloured Petri Nets ETAPS tool demonstration related to TACAS,” inTools and Algorithms for the Construction and Analysis of Systems (T. Margaria and W. Yi, eds.), (Berlin, Heidelberg), pp. 574–577, Sprin...

  12. [20]

    CPN IDE: An extensible replacement for CPN tools that uses access/CPN,

    E. Verbeek and D. Fahland, “CPN IDE: An extensible replacement for CPN tools that uses access/CPN,” inICPM 2021 Doctoral Consortium and Demo Track 2021(M. Jans, G. Janssenswillen, A. Kalenkova, and F. Maggi, eds.), CEUR Workshop Proc., pp. 29–30, CEUR-WS.org, 2021

  13. [21]

    Circle — USDC Terms — circle.com

    Circle, “Circle — USDC Terms — circle.com.” https://www.circle.com/ legal/usdc-terms, 2024. [Accessed 01-11-2024]

  14. [22]

    GPT-4o system card,

    OpenAI, A. Hurst, A. Lerer, A. P. Goucher, A. Perelman, A. Ramesh, A. Clark,et al., “GPT-4o system card,” 2024

  15. [23]

    Gemini 1.5: Unlocking multimodal understanding across millions of tokens of context,

    G. Team, P. Georgiev, V . I. Lei, R. Burnell, L. Bai, A. Gulati, G. Tanzer, et al., “Gemini 1.5: Unlocking multimodal understanding across millions of tokens of context,” 2024

  16. [24]

    Anthropic - Claude 3.5 Sonnet

    A. AI, “Anthropic - Claude 3.5 Sonnet.” https://www.anthropic.com/ news/claude-3-5-sonnet. [Accessed 01-11-2024]

  17. [25]

    The Llama 3 herd of models,

    A. Dubeyet al., “The Llama 3 herd of models,”arXiv preprint arXiv:2407.21783, 2024

  18. [26]

    Claude 3.5 sonnet model card addendum

    A. AI, “Claude 3.5 sonnet model card addendum.” https://www-cdn. anthropic.com/fed9cc193a14b84131812372d8d5857f8f304c52/Model Card Claude 3 Addendum.pdf, 2024

  19. [27]

    Plan-and-solve prompting: Improving zero-shot chain- of-thought reasoning by large language models,

    L. Wanget al., “Plan-and-solve prompting: Improving zero-shot chain- of-thought reasoning by large language models,” 2023

  20. [28]

    Chain-of-thought prompting elicits reasoning in large language models,

    J. Weiet al., “Chain-of-thought prompting elicits reasoning in large language models,”Advances in Neural Information Processing Systems, vol. 35, pp. 24824–24837, 2022

  21. [29]

    Evaluating software complexity measures,

    E. Weyuker, “Evaluating software complexity measures,”IEEE Trans. on Software Engineering, vol. 14, no. 9, pp. 1357–1365, 1988

  22. [30]

    Properties of software measures,

    D. A. Gustafson and B. Prasad, “Properties of software measures,” in Formal Aspects of Measurement(T. Denvir, R. Herman, and R. W. Whitty, eds.), (London), pp. 179–193, Springer London, 1992

  23. [31]

    Automatic smart contract generation through llms: When the stochastic parrot fails,

    F. Barb `ara, E. A. Napoli, V . Gatteschi, and C. Schifanella, “Automatic smart contract generation through llms: When the stochastic parrot fails,” in6th Distributed Ledger Technology Workshop, 2024

  24. [32]

    Manticore: A user-friendly symbolic execution framework for binaries and smart contracts,

    M. Mossberget al., “Manticore: A user-friendly symbolic execution framework for binaries and smart contracts,” in34th IEEE/ACM Int. Conf. on Automated Software Engineering (ASE), pp. 1186–1189, 2019

  25. [33]

    Making smart contracts smarter,

    L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor, “Making smart contracts smarter,” inProc. 2016 ACM SIGSAC Conf. on Computer and Communications Security, CCS ’16, p. 254–269, ACM, 2016

  26. [34]

    Symboleo: Towards a specification language for legal contracts,

    S. Sharifi, A. Parvizimosaed, D. Amyot, L. Logrippo, and J. Mylopoulos, “Symboleo: Towards a specification language for legal contracts,” in 2020 IEEE 28th Int. Requirements Engineering Conf. (RE), pp. 364– 369, Aug 2020

  27. [35]

    Subcontracting, assignment, and substitution for legal contracts in Symboleo,

    A. Parvizimosaed, S. Sharifi, D. Amyot, L. Logrippo, and J. Mylopoulos, “Subcontracting, assignment, and substitution for legal contracts in Symboleo,” inConceptual Modeling(G. Dobbie, U. Frank, G. Kappel, S. W. Liddle, and H. C. Mayr, eds.), (Cham), pp. 271–285, Springer Int....

  28. [36]

    On legal contracts, imperative and declarative smart contracts, and blockchain systems,

    G. Governatori, F. Idelberger, Z. Milosevic, R. Riveret, G. Sartor, and X. Xu, “On legal contracts, imperative and declarative smart contracts, and blockchain systems,”Artificial Intelligence and Law, vol. 26, pp. 377–409, 2018

  29. [37]

    From institutions to code: Towards automated generation of smart contracts,

    C. K. Frantz and M. Nowostawski, “From institutions to code: Towards automated generation of smart contracts,” inIEEE 1st Int. Workshops on Foundations and Applications of Self* Systems (FAS*W), pp. 210–215, 2016

  30. [38]

    SPESC: A Specifica- tion Language for Smart Contracts,

    X. He, B. Qin, Y . Zhu, X. Chen, and Y . Liu, “SPESC: A Specifica- tion Language for Smart Contracts,” inIEEE 42nd Annual Computer Software and Applications Conf. (COMPSAC), vol. 01, pp. 132–137, 2018

  31. [39]

    A model for verification and validation of law compliance of smart contracts in IoT environment,

    F. Amato, G. Cozzolino, F. Moscato, V . Moscato, and F. Xhafa, “A model for verification and validation of law compliance of smart contracts in IoT environment,”IEEE Trans. on Industrial Informatics, vol. 17, no. 11, pp. 7752–7759, 2021

  32. [40]

    A unifying model of legal smart contracts,

    J. Ladleif and M. Weske, “A unifying model of legal smart contracts,” inConceptual Modeling(A. H. F. Laender, B. Pernici, E.-P. Lim, and J. P. M. de Oliveira, eds.), (Cham), pp. 323–337, Springer Int. Publishing, 2019

Pith tools

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