arXiv Science⌕ Search

arXiv · 2610.27971

Execution-Time Validation of Context-Carrying Action Intents in Industrial Cyber-Physical Systems

Abstract

In industrial cells, commands from learned policies, operators and schedulers reach the controller after inference, confirmation and transport, and the plant may have changed meanwhile, for instance by an operator pause. Such a command is released, or takes effect, when it is no longer correct. We call this the execution gap and ask which component should make the last check, and against which version of which state. The Action Intent Schema (AIS) is a contract in which a producer states how long its decision stays valid and what it assumes. The runtime XAIR rechecks each intent before release, can commit its authorization atomically in the context store, and can release it as a version-conditional command, which the controller executes only if its version of the state is unchanged. In controlled ablations with declared ground truth on emulated and physical cells, OpenPLC and ARM and RISC-V boards, a check on a replica always left an unprotected interval: a pause written from a few to over 100ms after submission escaped it. Only a check in the scan of a software controller, either a controller-local interlock or the version-conditional command, closed the interval for the state that controller owns; only the version-conditional command also refused commands after a pause that had been undone. A global version revoked up to every valid command under unrelated updates. Versions scoped to what the intent reads, or to the truth of its predicates, did not; with continuous signals on the variables the intent reads, only the latter avoided false revocations, though it burdens the store as predicates accumulate. On one embedded-board core, XAIR validated 148-168 intents/s.

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Luca D'Agati, Giuseppe Tricomi, Fabio Orazio Mirto, Giovanni Merlino. 2026-10-20. Execution-Time Validation of Context-Carrying Action Intents in Industrial Cyber-Physical Systems. https://arxiv.org/abs/2610.27971

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

Foundational Refinement Proofs for EVM Bytecode, at the Price of Tokens

Relating executable code to a high-level model of its behavior has been a central concern of programming-language research for decades. Formally verified compilers, translation validators and certifying compilers address this problem through different trade-offs between proof effort, automation, generality, and the size of the trusted base. Recently, large language models (LLMs) have begun to change the economics of formal verification. Agentic proof development is now capable of producing machine-checked proofs, sometimes unsupervised, at a scale and speed that were previously out of reach. We propose a verification architecture that takes advantage of this shift. An executable obtains a machine-checked proof that it behaves according to a high-level model, independently of the compiler that produced it. The proof is written by an LLM agent. We evaluate the feasibility of this architecture for the Ethereum Virtual Machine (EVM). We build EquiVM, a foundational framework in Lean comprising an executable EVM semantics and a formal specification language, Stele, that gives a high-level authoritative model of the bytecode's behavior, but commits to no source language or compilation toolchain. We state what it means for EVM bytecode to refine a Stele spec and we build a proof library to facilitate proof construction. We evaluate the capabilities of frontier LLMs to construct such proofs, as well as the cost of proof production and repair. Our results show that agents prove 35 real production contracts end to end, without modifying their source or bytecode, among them core contracts of Safe, Morpho, Compound and Uniswap protocols, with bytecode of size close to the maximum the EVM allows. Several proofs need only the initial prompt, the rest a handful of human inputs, and existing proofs are repaired in a fraction of the original time when the source or the compiler configuration changes.

cs.PL↗

Noise-aware Verification and Synthesis of Quantum Programs

This work provides a comprehensive framework for noise-aware quantum program analysis, ranging from logical foundations to model checking and automated synthesis. While most research on quantum programming considers an idealized, noise-free semantics for quantum programs, we reason about quantum programs that are executed on real, noisy hardware. We use the error models published by quantum-hardware vendors to give a hardware-dependent semantics to quantum programs. We then present a noise-aware quantum Hoare logic with a relatively complete proof system. We finally use state-space exploration techniques for the hardware-aware verification and synthesis of loop-free quantum programs. In this way, we synthesize optimal, hardware-dependent solutions for parity bit-flip, GHZ state preparation, and other problems that commonly occur as subroutines in larger quantum algorithms. We evaluate our method on all 55 hardware specifications provided by the IBM Qiskit toolkit. Finally, we also show that classical probabilistic branching is needed for optimality in quantum programming.

cs.PL↗

Record Types Everywhere

This paper introduces a novel calculus that models first-class environments and function application paradigms using standard record types. By proposing new extensions to general record types, we achieve a design that is remarkably simple and principled. We formalise this design in a core calculus and prove several desirable properties, including type soundness, normalization, and a simulation of the simply typed lambda calculus. Additionally, we extend the design with mutable references. The calculus, its semantics, along with the extension, and all stated properties are fully mechanized in the Lean 4 proof assistant, alongside an interpreter formally verified to be equivalent to the operational semantics.

cs.PL↗