Vibe coding – accepting LLM-generated source from natural-language intent with minimal review – is fast and may be adequate for low-criticality consumer software. But for safety-critical systems governed by DO-178C, IEC 61508, or ISO 26262, it offers no path to certification: large language models (LLMs) provide no formal correctness guarantees, and existing remedies target verification-aware languages (Dafny, Verus, Lean) that are scarce in pretraining data and absent from industrial toolchains. This paper closes the gap. We present Forge (Formal method Oriented Refinement loop for GEnerated code): a closed-loop pipeline that guides vibe coding through formal verification using established Model-Driven Engineering (MDE) infrastructure. Through vibe coding, we generate Java source code; our pipeline then extracts – via model transformations – formal artefacts in three different formalisms, each checked by a complementary verifier: deductive verification (Dafny), Communicating Sequential Processes (CSP) refinement via the Failures-Divergences Refinement checker (FDR4), and theorem proving using Z-Machines in Isabelle; every verification failure becomes a structured correction prompt that drives the next code-generation iteration. The LLM is the draft generator, the MDE chain is the discriminator, and the developer never has to read the formal models. Empirically, we find that the pipeline produces standards-relevant verification evidence for LLM-generated Java – a step toward certification.

Robotics and Autonomous Systems are increasingly deployed in safety-critical domains, so that demonstrating their safety is essential. Assurance Cases (ACs) provide structured arguments supported by evidence, but generating and maintaining this evidence is labour-intensive, error-prone, and difficult to keep consistent as systems evolve. We present a model-based approach to systematically generating AC evidence by embedding formal verification into the assurance workflow. The approach addresses three challenges: systematically deriving formal assertions from natural language requirements using templates, orchestrating multiple formal verification tools to handle diverse property types, and integrating formal evidence production into the workflow. Leveraging RoboChart, a domain-specific modelling language with formal semantics, we combine model checking and theorem proving in our approach. Structured requirements are automatically transformed into formal assertions using predefined templates, and verification results are automatically integrated as evidence. Case studies demonstrate the effectiveness of our approach.

We explore the application of Constraint Programming (CP) tools to modelling state-based systems and verifying their properties. This includes finding execution traces leading to a particular state, and proving deadlock-freedom up to a given bound on the number of transitions. We present three distinct case studies. The first formulates a railway signal in the Essence CP modelling language, demonstrating use of Essence types and operators to model states, transitions, and invariants, in a system with a single finite-state automaton. The second case study is based on Dining Philosophers, and demonstrates effective CP modelling of a system with a large number of automata, synchronised on transitions. The third case study is part of the Alpha Algorithm, an example from swarm robotics. It introduces a clock, and has transitions with guards that refer to the clock. It also has triggers, representing sensor inputs, and non-deterministic waits, demonstrating that these concepts can be represented in a CP model. Finally we demonstrate that the CP approach is complementary to a model checking approach using FDR4. In many cases the CP approach can scale substantially better than the model checker, despite the CP toolchain being general-purpose, i.e. not explicitly designed for verifying properties of state-based models.

This paper presents a formalized analysis of the sigmoid function and a fully mechanized proof of the Universal Approximation Theorem (UAT) in Isabelle/HOL, a higher-order logic theorem prover. The sigmoid function plays a fundamental role in neural networks; yet, its formal properties, such as differentiability, higher-order derivatives, and limit behavior, have not previously been comprehensively mechanized in a proof assistant. We present a rigorous formalization of the sigmoid function, proving its monotonicity, smoothness, and higher-order derivatives. We provide a constructive proof of the UAT, demonstrating that neural networks with sigmoidal activation functions can approximate any continuous function on a compact interval. Our work identifies and addresses gaps in Isabelle/HOL's formal proof libraries and introduces simpler methods for reasoning about the limits of real functions. By exploiting theorem proving for AI verification, our work enhances trust in neural networks and contributes to the broader goal of verified and trustworthy machine learning.

This paper presents a formal modelling approach for BeliefDesire-Intention (BDI) agents using Isabelle/HOL and Z-Machines. The BDI architecture is widely used for modelling intelligent agents, where agents possess beliefs about the environment, desires or goals to achieve, and intentions to execute plans for goal attainment. The paper introduces a general-purpose model of the BDI architecture using Z-Machines. The modelling framework includes specifications for beliefs, actions, rules, plans, pattern matching, and rule applications. The proposed model can be used to formally verify BDI agents' behaviour using Hoare Logic and Isabelle/Z-Machines. This framework then contributes to advancing formal modelling and verification of agent-based systems, showing how we can integrate automated reasoning to establish invariant properties of agents with compositional techniques to prove more significant properties of BDI systems. We demonstrate the effectiveness of our approach through a case study of a nuclear inspector robot, showing how we can verify invariants and uncover bugs in the system's behaviour.

Model execution allows us to prototype and analyse software engineering models by stepping through their possible behaviours, using techniques like animation and simulation. On the other hand, deductive verification allows us to construct formal proofs demonstrating satisfaction of certain critical properties in support of high-assurance software engineering. To ensure coherent results between execution and proof, we need unifying semantics and automation. In this paper, we mechanise Interaction Trees (ITrees) in Isabelle/HOL to produce an execution and verification framework. ITrees are coinductive structures that allow us to encode infinite labelled transition systems, yet they are inherently executable. We use ITrees to create verification tools for stateful imperative programs, concurrent programs with message passing in the form of the CSP and Circus languages, and abstract system models in the style of the Z and B methods. We demonstrate how ITrees can account for diverse semantic presentations, such as structural operational semantics, a relational program model, and CSP's failures-divergences trace model. Finally, we demonstrate how ITrees can be executed using the Isabelle code generator to support the animation of models.

Verification of robotic systems that use neural networks is a challenge. In this paper, we present a formal technique supported by tools to model and verify control software involving neural networks. Our technique enables reasoning about the reactive, communication-based, properties of a system through a process-algebraic lens. We support our framework with a link to state-of-the-art ANN verification tools, using them to prove contextual properties of a neural network. Our approach is flexible, platform-independent, and focuses on the logic of neural network models, instead of on a training method or specific use case.

Modern machine learning pipelines are built on numerical algorithms. Reliable numerical methods are thus a prerequisite for trustworthy machine learning and cyber-physical systems. Therefore, we contribute a framework for verified numerical methods in Isabelle/HOL based on ITrees. Our user-friendly specification language enables the direct declaration of numerical programs that can be annotated with variants and invariants for reasoning about correctness specifications. The generated verification conditions can be discharged via automated proof methods and lemmas from the HOL-Analysis library. The ITrees foundation interacts with Isabelle's code generator to export source code. This provides an end-to-end path from formal specifications with machine-checked guarantees to executable sources. We illustrate the process of modelling numerical methods and demonstrate the effectiveness of the verification by focusing on two well-known methods, the bisection method and the fixed-point iteration method. We also contribute crucial extensions to the libraries of formalised mathematics required for this objective: higher-order derivatives and Taylor's theorem in Peano form. Finally, we qualitatively evaluate the use of the framework for verifying numerical methods.

In order to formally verify robotic controllers, we must tackle the inherent uncertainty of sensing and actuation in a physical environment. We can model uncertainty using stochastic hybrid systems, which combine discrete jumps with continuous, stochastic behaviour. The verification of these systems is intractable for state-exploration based approaches, so we instead propose a deductive verification approach. As a first step towards a deductive verification tool, we present a mechanisation of Brownian motion within Isabelle/HOL. For this, we mechanise stochastic kernels and Markov semigroups, which allow us to specify a range of processes with stationary, independent increments. Further, we prove the Kolmogorov-Chentsov theorem, which allows us to construct H\"older continuous modifications of processes that satisfy certain bounds on their expectation. This paves the way for modelling and verifying stochastic hybrid systems in Isabelle/HOL.

We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), a framework for the verification of cyber-physical systems. We describe the semantic foundations of the framework's formalisation in the Isabelle/HOL proof assistant. A user-friendly language specification based on a robust state model makes our framework flexible and adaptable to various engineering workflows. New additions to the framework increase both its expressivity and proof automation. Specifically, formalisations related to forward diamond correctness specifications, certification of unique solutions to ordinary differential equations (ODEs) as flows, and invariant reasoning for systems of ODEs contribute to the framework's scalability and usability. Various examples and an evaluation validate the effectiveness of our framework.

We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), an open, compositional and extensible framework for the verification of cyber-physical systems. We extend a previous semantic approach with methods and techniques that increase its expressivity, proof automation, and scalability to the level of state-of-the-art deductive verification tools. Our contributions include a user-friendly specification language, a flexible hybrid store model, including vectors and matrices, and separation-logic-style rules for local reasoning with hybrid stores using a novel form of differentiation called framed Fréchet derivatives. The formalisation of correctness specifications with forward predicate transformers, the certification of flows as unique solutions to systems of ordinary differential equations, and invariant reasoning for such systems also contribute to the scalability and usability of our framework. In combination, these features make our framework flexible and adaptable to several verification workflows. A suite of examples and hybrid systems verification benchmarks validate our framework relative to other state-of-the-art approaches.

Assurance cases are used to communicate and assess confidence in critical system properties, e.g., safety and security. Historically, assurance cases have been manually created documents, validated by engineers through lengthy and error-prone processes. Recently, system assurance practitioners have begun adopting model-based approaches to improve the efficiency and quality of system assurance activities. This becomes increasingly important, for example, to ensure the safety of robotics and autonomous systems (RASs), as they are adopted into society. Such systems can be highly complex, and so it is a challenge to manage the development life-cycle and improve efficiency, including coordination of validation activities, and change impact analysis in interconnected system assurance artifacts. However, adopting model-based approaches require skills in the model management languages, which system assurance practitioners may not be acquainted with. In this article, we contribute an automated validation framework for the model-based assurance cases, which promotes the usage of a constrained natural language (CNL), that can be automatically transformed and executed against engineering models involved in assurance case development. We apply our approach to a case study based on an autonomous underwater vehicle (AUV).

Probabilistic programming combines general computer programming, statistical inference, and formal semantics to help systems make decisions when facing uncertainty. Probabilistic programs are ubiquitous, including having a significant impact on machine intelligence. While many probabilistic algorithms have been used in practice in different domains, their automated verification based on formal semantics is still a relatively new research area. In the last two decades, it has attracted much interest. Many challenges, however, remain. The work presented in this paper, probabilistic unifying relations (ProbURel), takes a step towards our vision to tackle these challenges.Our work is based on Hehner's predicative probabilistic programming, but there are several obstacles to the broader adoption of his work. Our contributions here include (1) the formalisation of its syntax and semantics by introducing an Iverson bracket notation to separate relations from arithmetic; (2) the formalisation of relations using Unifying Theories of Programming (UTP) and probabilities outside the brackets using summation over the topological space of the real numbers; (3) the constructive semantics for probabilistic loops using Kleene's fixed-point theorem; (4) the enrichment of its semantics from distributions to subdistributions and superdistributions to deal with the constructive semantics; (5) the unique fixed-point theorem to simplify the reasoning about probabilistic loops; and (6) the mechanisation of our theory in Isabelle/UTP, an implementation of UTP in Isabelle/HOL, for automated reasoning using theorem proving.We demonstrate our work with six examples, including problems in robot localisation, classification in machine learning, and the termination of probabilistic loops.

Assurance cases are used to communicate and assess confidence in critical system properties such as safety and security. Historically, assurance cases have been manually created documents, which are evaluated by system stakeholders through lengthy and complicated processes. In recent years, model-based system assurance approaches have gained popularity to improve the efficiency and quality of system assurance activities. This becomes increasingly important, as systems becomes more complex, it is a challenge to manage their development life-cycles, including coordination of development, verification and validation activities, and change impact analysis in inter-connected system assurance artifacts. Moreover, there is a need for assurance cases that support evolution during the operational life of the system, to enable continuous assurance in the face of an uncertain environment, as Robotics and Autonomous Systems (RAS) are adopted into society. In this paper, we contribute ACCESS - Assurance Case Centric Engineering of Safety-critical Systems, an engineering methodology, together with its tool support, for the development of safety critical systems around evolving model-based assurance cases. We show how model-based system assurance cases can trace to heterogeneous engineering artifacts (e.g. system architectural models, system safety analysis, system behaviour models, etc.), and how formal methods can be integrated during the development process. We demonstrate how assurance cases can be automatically evaluated both at development and runtime. We apply our approach to a case study based on an Autonomous Underwater Vehicle (AUV).

The severity of recent vulnerabilities discovered on modern CPUs, e.g., Spectre [1], highlights how information leakage can have devas-tating effects to the security of computer systems. At the same time, it suggests that confidentiality should be promoted as a normal part of program verification, to discover and mitigate such vulnerabili-ties early in development. The theory we propose is primarily based on Bank's theory [2], a framework for reasoning about confidentiali-ty properties formalised in the Unifying Theories of Programming (UTP) [3]. We mechanised our encoding in the current implementa-tion of UTP in the Isabelle theorem prover, Isabelle/UTP [4]. We have identified some theoretical issues in Bank's original framework. Finally, we demonstrate how our mechanisation can be used to for-mally verify of some of the examples from Bank's work.

This paper reports on the Hybrid Systems Theorem Proving (HSTP) category in the ARCH-COMP Friendly Competition 2023. The characteristic features of the HSTP category remain as in the previous edition: HSTP focuses on flexibility of programming languages as structuring principles for hybrid systems, unambiguity and precision of program semantics, and mathematical rigor of logical reasoning principles. The benchmark set includes nonlinear and parametric continuous and hybrid systems and hybrid games, each in three modes: fully automatic verification, semi-automatic verification from proof hints, proof checking from scripted tactics. This instance of the competition focuses on presenting the differences between the provers on a subset of the benchmark examples.

We dedicate this paper with great respect and friendship to He Jifeng on the occasion of his 80th birthday. Our research group owes much to him. The authors have over 150 publications on unifying theories of programming (UTP), a research topic Jifeng created with Tony Hoare. Our objective is to recount the history of Circus (a combination of Z, CSP, Dijkstra’s guarded command language, and Morgan’s refinement calculus) and the development of Isabelle/UTP. Our paper is in two parts. (1) We first discuss the activities needed to model systems: we need to formalise data models and their behaviours. We survey our work on these two aspects in the context of Circus. (2) Secondly, we describe our practical implementation of UTP in Isabelle/HOL. Mechanising UTP theories is the basis of novel verification tools. We also discuss ongoing and future work related to (1) and (2). Many colleagues have contributed to these works, and we acknowledge their support.

RoboChart is a graphical language for model-based engineering of robotic systems, in the style of UML and SysML. It contains notations for data structures, system architecture, and the behaviour of individual robotic controllers using state machines. Crucially, RoboChart has a formal semantics in the CSP process algebra, which provides a precise foundation for software engineering and formal verification using model checking. However, due to state explosion, the application of model checking does not scale. In this paper, we contribute a compositional verification technique that uses Isabelle/HOL RoboChart state machines symbolically. Our technique uses state invariants to capture safety requirements over a very large or infinite state, similar to the B method, and is highly automated using Isabelle’s sledgehammer tool. We give a model transformation from the RoboTool development environment to Isabelle/HOL and apply this to several verification case studies.