Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)

• URL: http://arxiv.org/abs/2509.20421v2
• Date: Fri, 26 Sep 2025 09:51:15 GMT
• Title: Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)
• Authors: Reiner Hähnle, Cosimo Laneve, Adele Veschetti,
• Abstract summary: This paper presents a methodology to formally verify the correctness of Stipula contracts through translation into Java code annotated with Java Modeling Language specifications.<n>As a verification backend, the deductive verification tool KeY is used.
• Score: 0.2446948464551684
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Stipula is a domain-specific programming language designed to model legal contracts with enforceable properties, especially those involving asset transfers and obligations. This paper presents a methodology to formally verify the correctness of Stipula contracts through translation into Java code annotated with Java Modeling Language specifications. As a verification backend, the deductive verification tool KeY is used. Both, the translation and the verification of partial and total correctness for a large subset of Stipula contracts, those with disjoint cycles, is fully automatic. Our work demonstrates that a general-purpose deductive verification tool can be used successfully in a translation approach.

Related papers

• Uma Prova de Conceito para a Verificação Formal de Contratos Inteligentes [0.0]
  This work presents a proof of concept using the Relativized Contract Language (RCL) and the RECALL tool.<n>The study demonstrates the tool's capability to detect normative conflicts during the modeling phase.
  arXiv  Detail & Related papers  (2026-01-20T19:38:17Z)
• Advancing Automated In-Isolation Validation in Repository-Level Code Translation [9.753507630426832]
  Repository-level code translation aims to migrate entire repositories across programming languages while preserving functionality automatically.<n>This paper proposes TRAM, which combines context-aware type resolution with mock-based in-isolation validation.<n>TRAM demonstrates state-of-the-art performance in Java-to-Python translation, underscoring the effectiveness of its integration of RAG-based type resolution with reliable in-isolation validation.
  arXiv  Detail & Related papers  (2025-11-26T19:53:46Z)
• Formal verification in Solidity and Move: insights from a comparative analysis [0.40964539027092906]
  Solidity and Move are two contract languages with different designs and approaches to verification.<n>This paper investigates how the two languages impact verification, and what is the state-of-the-art of verification tools for the two languages.<n>Our investigation is supported by an open dataset of verification tasks performed in Certora and in the Aptos Move Prover.
  arXiv  Detail & Related papers  (2025-02-19T18:06:01Z)
• Lost in Translation, Found in Context: Sign Language Translation with Contextual Cues [56.038123093599815]
  Our objective is to translate continuous sign language into spoken language text.<n>We incorporate additional contextual cues together with the signing video.<n>We show that our contextual approach significantly enhances the quality of the translations.
  arXiv  Detail & Related papers  (2025-01-16T18:59:03Z)
• CRAT: A Multi-Agent Framework for Causality-Enhanced Reflective and Retrieval-Augmented Translation with Large Language Models [59.8529196670565]
  CRAT is a novel multi-agent translation framework that leverages RAG and causality-enhanced self-reflection to address translation challenges. Our results show that CRAT significantly improves translation accuracy, particularly in handling context-sensitive terms and emerging vocabulary.
  arXiv  Detail & Related papers  (2024-10-28T14:29:11Z)
• LegalPro-BERT: Classification of Legal Provisions by fine-tuning BERT Large Language Model [0.0]
  Contract analysis requires the identification and classification of key provisions and paragraphs within an agreement. LegalPro-BERT is a BERT transformer architecture model that we fine- tune to efficiently handle classification task for legal provisions.
  arXiv  Detail & Related papers  (2024-04-15T19:08:48Z)
• DELTA: Pre-train a Discriminative Encoder for Legal Case Retrieval via Structural Word Alignment [55.91429725404988]
  We introduce DELTA, a discriminative model designed for legal case retrieval. We leverage shallow decoders to create information bottlenecks, aiming to enhance the representation ability. Our approach can outperform existing state-of-the-art methods in legal case retrieval.
  arXiv  Detail & Related papers  (2024-03-27T10:40:14Z)
• Enhancing Translation Validation of Compiler Transformations with Large Language Models [5.103162976634333]
  This paper presents a framework that integrates Large Language Models (LLMs) into translation validation. We first utilize existing formal verification tools for translation validation. When formal verification tools are unable to confirm a transformation's soundness, our framework employs fine-tuned LLMs for prediction.
  arXiv  Detail & Related papers  (2024-01-30T07:24:04Z)
• SAILER: Structure-aware Pre-trained Language Model for Legal Case Retrieval [75.05173891207214]
  Legal case retrieval plays a core role in the intelligent legal system. Most existing language models have difficulty understanding the long-distance dependencies between different structures. We propose a new Structure-Aware pre-traIned language model for LEgal case Retrieval.
  arXiv  Detail & Related papers  (2023-04-22T10:47:01Z)
• Formal Modeling and Analysis of Legal Contracts using ContractCheck [0.0]
  textitContractCheck allows consistency analysis of legal contracts, in particular Sales Purchase Agreements (SPAs) The analysis relies on an encoding of the premises for the execution of the clauses of an SPA as well as the proposed consistency constraints using decidable fragments of first-order logic.
  arXiv  Detail & Related papers  (2022-12-06T22:03:11Z)
• Multilingual Extraction and Categorization of Lexical Collocations with Graph-aware Transformers [86.64972552583941]
  We put forward a sequence tagging BERT-based model enhanced with a graph-aware transformer architecture, which we evaluate on the task of collocation recognition in context. Our results suggest that explicitly encoding syntactic dependencies in the model architecture is helpful, and provide insights on differences in collocation typification in English, Spanish and French.
  arXiv  Detail & Related papers  (2022-05-23T16:47:37Z)
• Automatic Extraction of Rules Governing Morphological Agreement [103.78033184221373]
  We develop an automated framework for extracting a first-pass grammatical specification from raw text. We focus on extracting rules describing agreement, a morphosyntactic phenomenon at the core of the grammars of many of the world's languages. We apply our framework to all languages included in the Universal Dependencies project, with promising results.
  arXiv  Detail & Related papers  (2020-10-02T18:31:45Z)
• Multilingual Alignment of Contextual Word Representations [49.42244463346612]
  BERT exhibits significantly improved zero-shot performance on XNLI compared to the base model. We introduce a contextual version of word retrieval and show that it correlates well with downstream zero-shot transfer. These results support contextual alignment as a useful concept for understanding large multilingual pre-trained models.
  arXiv  Detail & Related papers  (2020-02-10T03:27:21Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.