Pith. sign in

REVIEW 4 major objections 5 minor 34 references

Logical foundations of Smart Contracts

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

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

Pith's one-line read Smart contracts can be given a formal, executable logic by modeling obligations as a Situation Calculus fluent.

desk verdict A thesis proposal that claims completed work but shows no technical content; the plan is plausible but unverifiable. read the letter →

arxiv 2502.09232 v1 pith:OZLKKVV6 submitted 2025-02-13 cs.LO cs.AI

Kalonji Kalala (University of Ottawa) This is my paper · ORCID
classification cs.LOcs.AI MSC 03B7068Q6068T27
keywords smartcontractssituationcalculusobligationdeonticlogicframeproblemsuccessorstateaxiomsformalverificationGOLOG
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

This paper proposes to give smart contracts a formal, executable semantics by modeling them in the Situation Calculus, a logic designed for reasoning about how actions change a world. The central move is to treat contractual obligations the way that logic already treats knowledge: add a dedicated obligation predicate, and write general rules describing how actions create and destroy obligations. With those rules, the author constructs 'basic contractual theories' that axiomatize legal contracts, represents contracts as programs in the GOLOG language, and argues that contract properties can then be proved automatically by regression back to the initial situation. If the proposal is right, a legal contract can be turned into a machine-checkable theory whose clauses are executable and verifiable, addressing an open problem in the area. The author reports the formalization of obligations as completed within the thesis, though it is not reproduced in this short paper.

What carries the argument

The central mechanism is an obligation fluent: a predicate that records, in each situation, which conditions an agent is obliged to bring about. It is equipped with successor state axioms written by analogy with the standard knowledge solution to the frame problem, so that the only actions that change the fluent are obligation-producing actions, and the fluent otherwise persists. These axioms are what turn a basic action theory into a basic contractual theory. The other load-bearing piece is the regression operator of the Situation Calculus, which takes a formula about a later situation and rewrites it, using the successor state axioms, into an equivalent formula about the initial situation; the paper relies on this to make contract properties automatically checkable.

What would settle it

Build the smallest possible contract theory with two actions, one that makes a payment obligatory and one that fulfills it, together with the proposed successor state axioms for the obligation fluent. If a query about the situation after the fulfillment action still yields that the payment is obligatory, or if a regression of that query differs from evaluating it directly in the situation, the analogy with knowledge fails. More generally, any basic contractual theory in which the successor state axioms let an obligation-producing action alter a fluent other than the obligation fluent would falsify the claim that obligations are isolated from the rest of the action theory.

Watch

Extended reading notes

Core claim

The paper's central claim is that smart contracts can be given logical foundations by reducing the notion of contractual obligation to a single new fluent in the Situation Calculus. Building on the established solution to the frame problem for knowledge, the author proposes that obligation-producing actions are governed by successor state axioms for this fluent: such actions make certain conditions obligatory, obligations persist through unrelated actions, and an action contrary to the obligation is what removes it. These axioms define 'basic contractual theories,' which the paper presents as the formal semantics of legal contracts. In the paper's account, a contract is a process in the Situation Calculus, written in GOLOG and executed by an interpreter, and properties of the contract are proved by the regression operator, which reduces a query about an execution situation to a query about the initial situation. The author states that this extension yields the intuitive properties of obligations and that regression remains a sound and complete reasoning mechanism for the extended language.

Load-bearing premise

The whole approach depends on an unproved analogy: that a new obligation predicate whose changes are specified in the same way as knowledge will behave like a real obligation, with actions creating it, unrelated actions leaving it alone, and only contradictory actions removing it, and that the standard regression method for reasoning about actions will still be correct for the extended language. The paper asserts these properties but does not supply the definitions or proofs.

Editorial extensions

If this is right

  • A legal contract can be expressed as a basic contractual theory, giving it a single formal meaning instead of an informal code description.
  • Contract properties such as 'payment becomes obligatory after delivery' can be checked automatically by regression on the theory.
  • Because the same theory is executed by the GOLOG interpreter, the specification and the implementation of a contract coincide.
  • Exceptions and subcontracts fit naturally into the same framework, since they are just additional actions and fluents in the logical language.
  • Contract verification becomes a logic problem: proving that a deployed contract satisfies its legal obligations is a theorem about its basic contractual theory.

Reading between the lines

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

  • Beyond the paper, the same extension-by-analogy could be tried for permissions, prohibitions, and powers, yielding a fuller deontic layer on top of the Situation Calculus rather than a single obligation predicate.
  • A natural testable extension is to implement the obligation successor state axioms on a small payment contract and check whether regression stays complete; a failure there would suggest restricting to a fragment of the language.
  • If the thesis matures into an implementation, it could supply a formal bridge from natural-language contracts through a legal-contract specification language to auditable blockchain code.
  • The proposal implicitly predicts that contract vulnerabilities will show up as logical consequences of the basic contractual theory, so a deployed contract that violates a proved property would be an implementation bug rather than a limitation of the logic.
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

4 major / 5 minor

Summary. The manuscript proposes to give logical foundations to smart contracts using the Situation Calculus and the GOLOG programming language. The intended approach is to extend Scherl and Levesque's solution to the frame problem for knowledge-producing actions to a new notion of obligation-producing actions, thereby obtaining 'basic contractual theories' that formalize legal contracts, an implementable GOLOG specification, and an obligation-based programming framework for verifying contract properties. The paper is a brief extended abstract: it surveys related work, states the problem, outlines the methodology, lists expected contributions, and reports on the current status of the research. It contains no formal definitions, axioms, theorems, proofs, or worked examples; the technical content that would support the central claims is entirely absent.

Significance. If the proposed extension succeeds, it would offer a uniform formal semantics for smart contracts, with the potential to support executable specifications and automated verification of contract properties in a well-studied action logic. The combination of deontic notions with Situation Calculus and GOLOG is a plausible and potentially valuable direction, building on a solid existing body of work. However, as it stands, the manuscript is a research proposal rather than a research contribution. No technical claim can be checked, and the significance of the approach cannot be assessed beyond the general interest of the idea. The paper explicitly claims that several steps of the research are complete (Section 7), so the absence of any formal development is a substantive gap, not merely a question of presentation.

major comments (4)
  1. [Sections 4 and 7 (Step 3)] The central technical claim is that obligations can be formalized by extending Scherl and Levesque's successor state axiom for knowledge to obligation-producing actions, but the manuscript never defines the obligation fluent, the class of obligation-producing actions, the successor state axiom for that fluent, or the underlying basic action theory. Without these definitions, the claimed 'intuitive properties' (obligation-producing actions affect only the new fluent and those fluents made obligatory, persistence unless a contrary action occurs) cannot be stated precisely, let alone proved. This is the load-bearing step of the entire proposal, and it is entirely missing.
  2. [Section 7 (Step 3), final sentence] The claim that 'Reiter's regression operator for reasoning about actions back to the initial situation is a reasoning mechanism for this setting as well' is unsupported. Regression is sound and complete only for basic action theories whose successor state axioms have a specific syntactic form. Adding a modality for obligations may break this form, for instance if the successor state axiom for the obligation fluent quantifies over future actions or mentions fluents within its own scope. The author must state the axiom and prove that the resulting theory is a basic action theory (or otherwise justify that regression remains applicable).
  3. [Section 7 (Step 4)] The proposed translation from Symboleo specifications to Situation Calculus theories is mentioned only in one sentence. Since the paper promises 'implementable specifications' and automatic checking of contract properties, the translation relation, the syntactic categories of Symboleo being covered, and at least one worked example are necessary to evaluate whether the approach is feasible and whether the resulting theories have the claimed properties.
  4. [Section 7 (Steps 2-5)] The 'Current Status of the Research' section states that steps (2)-(4) and parts of step (5) have been completed, but none of the corresponding definitions, theorems, or artifact descriptions appear in the paper. If this is an extended abstract of a thesis, the author should either include the key technical content or explicitly state that the full development is forthcoming; as written, the claim of completion is unverifiable and is not a substitute for presenting the results.
minor comments (5)
  1. [Abstract] The sentence 'Smart contracts are going to be implement with Golog (written en Prolog)' contains grammatical errors and a typo; it should read, for example, 'Smart contracts are going to be implemented in GOLOG (written in Prolog).'
  2. [Section 1] The phrase 'le formal languages are equipped...' contains a French article; it should be 'the formal languages...'.
  3. [Section 3] The text says 'the situation calculation' in Section 7; the correct term is 'situation calculus'.
  4. [Section 5] The description of basic action theories as 'mostly first-order' should be made precise, since the foundational axioms typically include a second-order induction axiom; the author should clarify which version of the theory is being used.
  5. [References] Several references are incomplete or contain visible errors (e.g., reference [3] has a garbled title); the reference list should be carefully checked against the original sources.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the paper is a proposal without a derivation chain, so no claim reduces by construction to its own inputs.

full rationale

This short ICLP 'thesis proposal' paper does not contain a derivation. Section 4 states an intended approach—extending Scherl and Levesque's solution to the frame problem for knowledge to obligations—and Section 7 reports which chapters have been completed, asserting that the formalization 'yields intuitive properties' and that 'Reiter's regression operator ... is a reasoning mechanism for this setting as well.' These are claims about planned or summarized work, not results derived in this paper. There is no equation, no fitted parameter, no successor state axiom for the obligation fluent, and no proof presented; therefore there is no specific reduction to exhibit. The load-bearing step is an analogy with Scherl and Levesque's knowledge solution, and the concern that this analogy might fail (e.g., because obligations may require quantification over future actions, breaking the basic action theory form needed for regression) is a correctness or completeness risk, not a circularity. The paper also does not rely on self-citation: the cited prior work is external (Reiter, Scherl and Levesque), and the author has no overlapping prior publication invoked as authority. No step renames an existing result, imports a uniqueness theorem, or equates an output with an input by definition. Thus the appropriate finding is no significant circularity, score 0. If the later technical chapters define an obligation fluent by a successor state axiom that is then shown to satisfy the claimed properties, a future audit should check whether those properties are stipulated in the axiom rather than proved, but no such circularity is present in this manuscript.

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

The paper contains no formal result, so the ledger itemizes planned or asserted ingredients, not actual ones. The central proposal depends on the obligation fluent, obligation-producing actions, and an assumed extension of the regression mechanism, none of which are demonstrated here.

assumptions (4)
  • ad hoc to paper Obligations can be modeled by extending Scherl and Levesque's solution to knowledge-producing actions via a newly introduced fluent for obligation.
    Section 4 and Section 7 Step 3 assert this extension is the core idea, but no axioms or semantics are given.
  • domain assumption Situation Calculus basic action theories (Reiter) provide a suitable base for deontic reasoning.
    Section 3 and Section 5 take Reiter's basic action theory as the background formalism without argument.
  • domain assumption Symboleo contracts can be systematically translated into Situation Calculus specifications.
    Section 7 Step 4 plans this translation; no mapping is shown.
  • ad hoc to paper Reiter's regression operator remains a reasoning mechanism after adding the obligation fluent.
    Section 7 Step 3 asserts this as a result but no proof is included.
invented entities (2)
  • Obligation fluent
    purpose: A new situation calculus fluent intended to represent obligations of agents; central to the proposed formalization.
    Section 7 Step 3 says obligation-producing actions affect a newly introduced fluent, but no formal definition, successor state axiom, or property proof appears in the paper.
  • Obligation-producing actions
    purpose: Actions that enact obligations on the agent performing them; the proposed extension of Scherl and Levesque.
    Section 7 Step 3 introduces this action class; no formal characterization, no examples, and no semantics are given.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Logical foundations of Smart Contracts." pith.science (2026). https://pith.science/paper/OZLKKVV6

@misc{pith2026250209232,
  author       = {Pith},
  title        = {Pith review of: Logical foundations of Smart Contracts},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/OZLKKVV6}},
  note         = {Machine review of arXiv:2502.09232}
}
read the original abstract

Nowadays, sophisticated domains are emerging which require appropriate formalisms to be specified accurately in order to reason about them. One such domain is constituted of smart contracts that have emerged in cyber physical systems as a way of enforcing formal agreements between components of these systems. Smart contracts self-execute to run and share business processes through blockchain, in decentralized systems, with many different participants. Legal contracts are in many cases complex documents, with a number of exceptions, and many subcontracts. The implementation of smart contracts based on legal contracts is a long and laborious task, that needs to include all actions, procedures, and the effects of actions related to the execution of the contract. An ongoing open problem in this area is to formally account for smart contracts using a uniform and somewhat universal formalism. This thesis proposes logical foundations to smart contracts using the Situation Calculus, a logic for reasoning about actions. Situation Calculus is one of the prominent logic-based artificial intelligence approaches that provides enough logical mechanism to specify and implement dynamic and complex systems such as contracts. Situation Calculus is suitable to show how worlds dynamically change. Smart contracts are going to be implement with Golog (written en Prolog), a Situation Calculus-based programming language for modeling complex and dynamic behaviors.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

34 extracted references · 31 canonical work pages

  1. [4]

    Daskalopulu & M.J

    A. Daskalopulu & M.J. Sergot (1997): The Representation of Legal Contracts . AI Soc. 11(1), pp. 6–17, doi:10.1007/BF02812435

    work page doi:10.1007/bf02812435 1997

  2. [1]

    Azzopardi, G.J

    S. Azzopardi, G.J. Pace & F. Schapachnik (2018): On observing contracts: Deontic contracts meet smart contracts. Frontiers in Artificial Intelligence and Applications 313(December), pp. 21–30, doi:10.3233/978- 356 Logical Foundations of Smart Contracts 1-61499-935-5-21

    doi:10.3233/978- 2018

  3. [2]

    Languages for Smart and Computable Contracts

    C.D. Clack (2021): Languages for Smart and Computable Contracts . CoRR abs/2104.03764. arXiv:2104.03764

    work page Pith review arXiv 2021

  4. [3]

    A. Daskalopulu (2019): Logic-Based Tools for the Analysis and Representation of Legal Contracts Logic- Based Tools for the Analysis and Representation of Legal Contracts Aspassia-Kaliopi Daskalopulu Submitted in fulfilment of the requirements for the award of the degree of Docto(October 2009)

    work page 2019

  5. [5]

    Dorri, S.S

    A. Dorri, S.S. Kanhere, R. Jurdak & P. Gauravaram (2017):Blockchain for IoT security and privacy: The case study of a smart home. In: 2017 IEEE international conference on pervasive computing and communications workshops (PerCom workshops), IEEE, pp. 618–623, doi:10.1109/PERCOMW.2017.7917634

    work page arXiv 2017

  6. [6]

    Elsden, A

    C. Elsden, A. Manohar, J. Briggs, M. Harding, C. Speed & J. Vines (2018): Making sense of blockchain applications: A typology for HCI. In: Proceedings of the 2018 chi conference on human factors in computing systems, pp. 1–14, doi:10.1145/3173574.3174032

    work page arXiv 2018

  7. [7]

    Giannikis & A

    G.K. Giannikis & A. Daskalopulu (2006): Defeasible Reasoning with e-Contracts . In: Proceedings of the 2006 IEEE/WIC/ACM International Conference on Intelligent Agent Technology, Hong Kong, China, 18-22 December 2006, IEEE Computer Society, pp. 690–694, doi:10.1109/IAT.2006.51

    work page doi:10.1109/iat.2006.51 2006

  8. [8]

    Governatori, F

    G. Governatori, F. Idelberger, Z. Milosevic, R. Riveret, G. Sartor & X. Xu (2018): On legal contracts, imperative and declarative smart contracts, and blockchain systems . Artif. Intell. Law 26(4), pp. 377–409, doi:10.1007/s10506-018-9223-3

    doi:10.1007/s10506-018-9223-3 2018

Show all 34 references
  1. [9]

    Han, R.K

    H. Han, R.K. Shiwakoti, R. Jarvis, C. Mordi & D. Botchie (2023): Accounting and auditing with blockchain technology and artificial Intelligence: A literature review . International Journal of Accounting Information Systems 48, p. 100598, doi:10.1016/j.accinf.2022.100598

    2023

  2. [10]

    Hofmann, T

    T. Hofmann, T. Niemueller, J. Claßen & G. Lakemeyer (2016):Continual planning in Golog. In: Proceedings of the AAAI Conference on Artificial Intelligence, 30

    2016

  3. [11]

    Krishna & K

    P.R. Krishna & K. Karlapalem (2008): Electronic Contracts. IEEE Internet Comput. 12(4), pp. 60–68, doi:10.1109/MIC.2008.77

    2008 doi

  4. [12]

    de Kruijff & H

    J.T. de Kruijff & H. Weigand (2019): Introducing CommitRuleML for Smart Contracts. In P. Johannesson, B. Andersson & H. Weigand, editors: Short Paper Proceedings of the 13th International Workshop on Value Modeling and Business Ontologies, VMBO, 2019, Stockholm, Sweden, March ...

    2019

  5. [13]

    Levesque, R

    H.J. Levesque, R. Reiter, Y . Lespérance, F. Lin & R.B. Scherl (1997): GOLOG: A Logic Programming Language for Dynamic Domains. J. Log. Program. 31(1-3), pp. 59–83, doi:10.1016/S0743-1066(96)00121- 5

    1997 doi

  6. [14]

    McCarthy (1963): Situations, actions, and causal laws

    J. McCarthy (1963): Situations, actions, and causal laws. Technical Report, STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

    1963

  7. [15]

    McIlraith & T.C

    S. McIlraith & T.C. Son (2001): Adapting Golog for programming the semantic web. In: Fifth International Symposium on Logical Formalizations of Commonsense Reasoning, pp. 195–202

    2001

  8. [16]

    Monrat, O

    A.A. Monrat, O. Schelén & K. Andersson (2019): A Survey of Blockchain From the Per- spectives of Applications, Challenges, and Opportunities . IEEE Access 7, pp. 117134–117151, doi:10.1109/ACCESS.2019.2936094

    2019

  9. [17]

    Mourtzis, J

    D. Mourtzis, J. Angelopoulos & N. Panopoulos (2023): Blockchain integration in the era of industrial meta- verse. Applied Sciences 13(3), p. 1353, doi:10.3390/app13031353

    2023 doi

  10. [18]

    Panarello, N

    A. Panarello, N. Tapas, G. Merlino, F. Longo & A. Puliafito (2018): Blockchain and IoT Integration: A Systematic Survey. Sensors 18(8), p. 2575, doi:10.3390/s18082575

    2018 doi

  11. [19]

    Parvizimosaed (2020): Towards the Specification and Verification of Legal Contracts

    A. Parvizimosaed (2020): Towards the Specification and Verification of Legal Contracts. 28th IEEE Interna- tional Requirements Engineering Conference (RE’20). IEEE CS. Kalonji Kalala 357

    2020

  12. [20]

    Parvizimosaed, S

    A. Parvizimosaed, S. Sharifi, D. Amyot, L. Logrippo & J. Mylopoulos (2020): Subcontracting, Assign- ment, and Substitution for Legal Contracts in Symboleo . In G. Dobbie, U. Frank, G. Kappel, S.W. Lid- dle & H.C. Mayr, editors: Conceptual Modeling - 39th International Conferen...

    2020 doi

  13. [21]

    Pirri & R

    F. Pirri & R. Reiter (1999): Some contributions to the metatheory of the situation calculus . Journal of the ACM (JACM)46(3), pp. 325–361, doi:10.1145/316542.316545

    1999

  14. [22]

    Rahman, M.M

    M.A. Rahman, M.M. Rashid, M.S. Hossain, E. Hassanain, M.F. Alhamid & M. Guizani (2019): Blockchain and IoT-Based Cognitive Edge Framework for Sharing Economy Services in a Smart City . IEEE Access 7, pp. 18611–18621, doi:10.1109/ACCESS.2019.2896065

    2019

  15. [23]

    Ramamurthy (2020): Blockchain in action

    B. Ramamurthy (2020): Blockchain in action. Manning Publications

    2020

  16. [24]

    Reiter (2001): Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems

    R. Reiter (2001): Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems. The MIT Press, MIT Press, doi:10.7551/mitpress/4074.001.0001

    2001 doi

  17. [25]

    Reiter (1991): The Frame Problem in the Situation Calculus: A Simple Solution (Sometimes) and a Completeness Result for Goal Regression

    R. Reiter (1991): The Frame Problem in the Situation Calculus: A Simple Solution (Sometimes) and a Completeness Result for Goal Regression . In V . Lifschitz, editor: Artificial and Mathematical Theory of Computation, Papers in Honor of John McCarthy on the occasion of his six...

    1991 doi

  18. [26]

    Reiter (1993): Proving properties of states in the situation calculus

    R. Reiter (1993): Proving properties of states in the situation calculus . Artificial Intelligence 64(2), pp. 337–351, doi:10.1016/0004-3702(93)90109-O

    1993 doi

  19. [27]

    Scherl & H.J

    R.B. Scherl & H.J. Levesque (2003): Knowledge, action, and the frame problem . Artificial Intelligence 144(1-2), pp. 1–39, doi:10.1016/S0004-3702(02)00365-X

    2003 doi

  20. [28]

    Sharifi, A

    S. Sharifi, A. Parvizimosaed, D. Amyot, L. Logrippo & J. Mylopoulos (2020): Symboleo: towards a specifi- cation language for legal contracts. In: 2020 IEEE 28th International Requirements Engineering Conference (RE), IEEE, pp. 364–369, doi:10.1109/RE48521.2020.00049

    2020

  21. [29]

    Sharifi (2020): Smart Contracts : from Formal Specification to Blockchain Code

    S.S. Sharifi (2020): Smart Contracts : from Formal Specification to Blockchain Code

    2020

  22. [30]

    Surden (2012): Computable contracts

    H. Surden (2012): Computable contracts. UCDL Rev. 46, p. 629

    2012

  23. [31]

    Tolmach, Y

    P. Tolmach, Y . Li, S. Lin, Y . Liu & Z. Li (2020): A Survey of Smart Contract Formal Specification and Verification. CoRR abs/2008.02712. arXiv:2008.02712

    2020 arXiv

  24. [32]

    J. Xu, C. Wang & X. Jia (2023): A survey of blockchain consensus protocols . ACM Computing Surveys 55(13s), pp. 1–35, doi:10.1145/3477138

    2023 doi

  25. [33]

    X. Yue, H. Wang, D. Jin, M. Li & W. Jiang (2016): Healthcare data gateways: found healthcare intelligence on blockchain with novel privacy risk control. Journal of medical systems 40, pp. 1–8, doi:10.1007/s10916- 016-0574-6

    2016 doi

  26. [34]

    Zheng, S

    Z. Zheng, S. Xie, H.-N. Dai, X. Chen & H. Wang (2018):Blockchain challenges and opportunities: A survey. International journal of web and grid services 14(4), pp. 352–375, doi:10.1504/IJWGS.2018.095647

    2018

Pith tools

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