Legal contracts are written in natural language, but automated compliance monitoring requires formal, executable specifications. The Symboleo ecosystem — a formal specification language for legal contracts, the SymboleoPC property checker, the Symboleo2SC code generator, and the CNL-based refinement formalizer SymboleoNLP, integrated in a 2025 web-based environment — currently bridges this gap only under a controlled natural language (CNL): event descriptions must be simple active-form statements, and conditional refinements must be event-based. The source paper (Meloche et al., 2025) poses as open problems the extension of this formalization to realistic contract language — event descriptions with subordinate clauses, negation, and conjunction, empirically derived from real contract data, together with state-based conditionals — and the relaxation of the CNL toward freeform input, possibly via large language models (LLMs), without unacceptable loss of mapping precision. Follow-up work by the same group reports early LLM experiments on whole-specification generation (Zitouni et al., 2025) and a preliminary LLM-plus-compiler-feedback repair agent (Singh et al., 2025), both explicitly preliminary; no published work yet covers the richer event semantics, the state-based conditionals, or freeform refinement input. The problem remains open.

Background

Legal contracts state obligations (duties a party must fulfill) and powers (rights, such as terminating the contract or charging a penalty, that a party may exercise when an obligation is violated). Because contracts are drafted in natural language, detecting violations early is hard; smart contracts — programs on a blockchain platform such as Hyperledger Fabric (a permissioned, consortium-oriented blockchain) — can monitor contract performance in a tamper-resistant way and automate violation handling. The obstacle is the gap between natural-language contract text and executable monitoring code.

The Symboleo research line addresses this gap with an intermediate formal layer. Symboleo is a first-order, time-based specification language built on a legal-contract ontology of parties, roles, assets, events, obligations, and powers (Parvizimosaed et al., 2022). A Symboleo specification can be checked against desirable properties expressed in Linear Temporal Logic (LTL) or Computation Tree Logic (CTL) — standard temporal logics for reasoning about how propositions evolve over time — using the model checker SymboleoPC, and can be compiled into monitoring smart contracts for Hyperledger Fabric by the code generator Symboleo2SC (Rasti et al., 2025; Parvizimosaed et al., 2025).

Writing Symboleo specifications by hand still demands formal-methods expertise, so Meloche, Amyot and Mylopoulos (2023) introduced a template-based approach: an unrefined natural-language contract template T is manually formalized once as a specification S(T); contract authors then state refinements C of the template — typically linguistic adjuncts, i.e. sentence components that add information (about time, place, or manner) and can be removed without breaking the sentence, such as "between [START_DATE] and [END_DATE]" — in a controlled natural language (CNL), an engineered subset of natural language designed to have unambiguous interpretations; the refined specification S(C) is then generated automatically. The tool SymboleoNLP implements this for temporal and conditional refinements (Meloche et al., 2024), and the source paper (Meloche et al., 2025) integrates SymboleoNLP with a web-based specification editor (SymboleoWeb) and Symboleo2SC into an end-to-end authoring environment, evaluated on a transactive-energy contract — a contract for trading energy between prosumers (consumers who also produce energy) and buyers.

The source states the current limits of this pipeline precisely. First, the events that can be represented are restricted to simple events in active form: event predicates and conditional triggers cannot be written from contract language containing subordinate clauses, negation, or conjunction, and the authors call for a more sophisticated event specification to be empirically derived from real contract data. Second, conditional refinements are restricted to conditionals about events, so state-based conditions — for example, "if the voltage of the dispatched energy is not within certain bounds" — cannot be expressed. Third, SymboleoNLP operates with a CNL precisely because it yields predictable mappings to the formal specification; the authors pose as an open question whether the input language can be relaxed toward freeform text — suggesting large language models (LLMs) as a possible route — without an unacceptable loss of mapping precision, where precision is assessed by the field's convention of manual expert review of generated specifications against an error taxonomy. Early evidence that this trade-off is real but unmeasured comes from the same group: LLM experiments generating whole Symboleo specifications from English contracts (Zitouni et al., 2025) showed promising but error-prone output, with grammar/syntax adherence problems and environment-variable identification failures in 49% of cases, and a follow-up repair agent combining LLMs with compiler feedback (Singh et al., 2025) reported only preliminary case-study results.

Problem Statement

Extend the reliable formalization of natural-language contract language into Symboleo beyond the current controlled natural language, as posed by Meloche et al. (2025). Concretely: (a) derive, empirically from real contract data, a more sophisticated event specification so that event predicates and conditional triggers can be formalized from contract language containing subordinate clauses, negation, and conjunction (the current tooling accepts only simple events in active form); (b) enable refinements expressing state-based conditionals, where the condition concerns the state of the world (e.g. the voltage of dispatched energy being outside given bounds) rather than only the occurrence of events; and (c) relax the controlled-natural-language constraint on refinement input toward freeform text without unacceptable loss of mapping precision, i.e. the generated Symboleo specifications must still faithfully encode the clause's obligations, powers, events, and conditional triggers. These three targets jointly serve one objective: letting contract authors formalize realistic contract language into Symboleo reliably, so that the formalization no longer diverges from the parties' declared intent at authoring time, with the refined specifications remaining well-formed for SymboleoPC verification and Symboleo2SC code generation.

References

  1. Meloche, R., Sivakumar, D., Anda, A.A., Alfuhaid, S., Amyot, D., Logrippo, L., Mylopoulos, J. (2025). A Web-Based Environment for the Specification and Generation of Smart Legal Contracts. arXiv:2509.11258, DOI 10.48550/arXiv.2509.11258, https://arxiv.org/abs/2509.11258
  2. Meloche, R., Amyot, D., Mylopoulos, J. (2023). Towards Legal Contract Formalization with Controlled Natural Language Templates. In: 2023 IEEE 31st International Requirements Engineering Conference (RE), pp. 317–322. DOI 10.1109/RE57278.2023.00042, https://doi.org/10.1109/RE57278.2023.00042
  3. Meloche, R., Amyot, D., Mylopoulos, J. (2024). SymboleoNLP: A Tool for Generating Formal Specifications from Legal Contract Templates. In: 2024 IEEE 32nd International Requirements Engineering Conference (RE). DOI 10.1109/RE59067.2024.00062, https://doi.org/10.1109/RE59067.2024.00062
  4. Parvizimosaed, A., Sharifi, S., Amyot, D., Logrippo, L., Roveri, M., Rasti, A., Roudak, A., Mylopoulos, J. (2022). Specification and analysis of legal contracts with Symboleo. Software and Systems Modeling 21(6), pp. 2395–2427. DOI 10.1007/s10270-022-01053-6, https://doi.org/10.1007/s10270-022-01053-6
  5. Rasti, A., Anda, A.A., Alfuhaid, S., Parvizimosaed, A., Amyot, D., Roveri, M., Logrippo, L., Mylopoulos, J. (2025). Automated generation of smart contract code from legal contract specifications with Symboleo2SC. Software and Systems Modeling 24(4), pp. 1127–1156. DOI 10.1007/s10270-024-01187-9, https://doi.org/10.1007/s10270-024-01187-9
  6. Parvizimosaed, A., Roveri, M., Rasti, A., Anda, A.A., Alfuhaid, S., Amyot, D., Logrippo, L., Mylopoulos, J. (2025). SymboleoPC: checking properties of legal contracts. Software and Systems Modeling 24(4), pp. 1093–1126. DOI 10.1007/s10270-024-01180-2, https://doi.org/10.1007/s10270-024-01180-2
  7. Zitouni, M.N., Anda, A.A., Rajpal, S., Amyot, D., Mylopoulos, J. (2025). Towards the LLM-Based Generation of Formal Specifications from Natural-Language Contracts: Early Experiments with Symboleo. In: 2025 IEEE/ACM Requirements Engineering for AI-powered SoftwarE (RAISE), co-located with ICSE. DOI 10.1109/RAISE66696.2025.00006 (preprint arXiv:2411.15898), https://doi.org/10.1109/RAISE66696.2025.00006
  8. Singh, G., Rajpal, S., Anda, A.A., Alfuhaid, S., Amyot, D., Mylopoulos, J., Roveri, M. (2025). Towards an LLM-Based Auto-Corrector Agent for Symboleo Specifications. In: 2025 IEEE International Conference on Collaborative Advances in Software and COmputiNg (CASCON). DOI 10.1109/CASCON66301.2025.00124, https://doi.org/10.1109/CASCON66301.2025.00124
  9. Alfuhaid, S. (2025). Towards Secure and Interactive Smart Contract Code from Formal Symboleo Specifications. In: 2025 IEEE/ACM 47th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion). DOI 10.1109/ICSE-Companion66252.2025.00024, https://doi.org/10.1109/ICSE-Companion66252.2025.00024
  10. Mylopoulos, J., Alfuhaid, S., Amyot, D., Anda, A.A., Logrippo, L., Meloche, R., Rahimi-Kian, A., Rajpal, S., Roveri, M., Sivakumar, D., Sousa-Dias, D. (2024). Engineering Smart Contracts with Symboleo: Progress Report 2024. In: CASCON 2024. DOI 10.1109/CASCON62161.2024.10838220, https://doi.org/10.1109/CASCON62161.2024.10838220
  11. Lourenço, L.M., Bezerra, C., Marques, A.P. (2026). Quality Evaluation of Software Functional Requirements Generated by LLMs: A Systematic Mapping Study. In: Simpósio Brasileiro de Sistemas de Informação (SBSI). DOI 10.5753/sbsi.2026.248317, https://doi.org/10.5753/sbsi.2026.248317