Short Version of VERIFAI2026 Paper -- Learning Infused Formal Reasoning: Contract Synthesis, Artefact Reuse and Semantic Foundations

TL;DR

This paper proposes Learning-Infused Formal Reasoning (LIFR), integrating machine learning with formal verification to automate contract synthesis, reuse artifacts, and establish semantic foundations for scalable, knowledge-driven system verification.

Contribution

It introduces a novel framework combining ML and formal methods for automated specification generation, artifact reuse, and semantic grounding based on UTP and institutions.

Findings

Framework for automated contract synthesis from natural language

Semantic reuse of verification artifacts via graph matching and embeddings

Semantic foundations grounded in UTP and the Theory of Institutions

Abstract

Artificial intelligence systems have achieved remarkable capability in natural language processing, perception and decision-making tasks. However, their behaviour often remains opaque and difficult to verify, limiting their applicability in safety-critical systems. Formal methods provide mathematically rigorous mechanisms for specifying and verifying system behaviour, yet the creation and maintenance of formal specifications remains labour intensive and difficult to scale. This paper outlines a research vision called Learning-Infused Formal Reasoning (LIFR), which integrates machine learning techniques with formal verification workflows. The framework focuses on three complementary research directions: automated contract synthesis from natural language requirements, semantic reuse of verification artifacts using graph matching and learning-based embeddings, and mathematically grounded semantic foundations based on the Unifying Theories of Programming (UTP) and the Theory of Institutions. Together these research threads aim to transform verification from isolated correctness proofs into a cumulative knowledge-driven process where specifications, contracts and proofs can be synthesised, aligned and reused across systems.