Papers

Quantum algorithms promise advantages beyond classical reach, but running them on error-corrected hardware requires translating Boolean specifications into reversible circuits, and the resources that translation demands determine what is executable. Established methods minimize a Boolean expression and map it to a circuit, assuming the minimized form is best. Here we show that minimized expressions retain algebraic structure minimization cannot reach, arising from containment and complementary-polarity relationships among their terms, and that extracting it yields circuits cheaper to execute despite having more operations. The decisive quantity is not a circuit's operation count but the control count of its widest operation, a superlinear cost; extracting shared factors trades a few wide operations for many narrow ones and reduces qubit count. Across benchmarks and oracles from quantum search and factoring algorithms, at the representation level the transformation never increases either cost measure, a guarantee from its construction. Translation to an executable circuit returns part of that advantage, since auxiliary lines must be uncomputed, yet the factorized circuit still left a leading circuit-level optimizer reaching lower final counts, and faster, than unaided. The representation of a computation is therefore itself a resource, optimizable before compilation and distinct from both logic minimization and circuit-level optimization.

A functor is a familiar model of an implementation, where every operation in a specification is assigned a concrete instantiation at the outset. But some tasks are less eager: we often want to assemble systems while leaving backend choices such as data representations and algorithms for later. We observe that cofunctors admit a direct reading as such partial implementations, which are implementations whose extra argument is a state-dependent family of deferred choices. While cofunctors (also called retrofunctors) are not novel, their conceptual and purposive reading in this manner appears to be.

We introduce a new family of benchmarks for the problem of diagrammatic equivalence between circuits. Three variants of this problem are considered, ranging from basic to challenging, and benchmarks are generated for each variant. We provide first-order encodings in both TPTP and SMT-LIB formats, together with scripts that automatically generate benchmark instances, and evaluate these benchmarks on state-of-the-art automated theorem provers and SMT solvers.

Deep generative models such as flow matching and diffusion models have shown potential for learning complex dynamical systems, but typically act as black boxes that neglect underlying physical structure, while physics-based models governed by partial differential equations are often incomplete due to missing source terms, or uncertain parametrisations. We present Climate Physics Dynamic Matching (ClimPhyDM), a variational simulation-free dynamics informed framework for weather forecasting that combines an advection-type physics prior with data-driven components in a variational framework. % to capture the stochasticity and multi-modality of unresolved atmospheric dynamics. On the ERA5 benchmark at hourly (42-hour) and monthly (5-month) resolutions, ClimPhyDM outperforms ClimODE, and GB-DM, keeping the lower error at extended horizon, indicating improved temporal stability and resistance to error accumulation, while its simulation-free paradigm also enables training on a single modest 12 GB consumer GPU.

An automated theorem prover builds a proof step by step, choosing at each point what to add and what to remove. We cast this construction as a policy acting in a transition system induced by a formal calculus, which fixes which steps are sound: for clausal connection tableaux, leanCoP-style search and plCoP/rlCoP-style planning then become stateful policies over one interface, and policy-learning methods apply directly. We equip such policies with a graph neural network that scores proof edits from structure that transfers across problems, train it by imitation learning from found proofs, and measure how performance holds as we remove search scaffolding, from full symbolic backtracking to a policy the network drives alone. Within a fixed step budget on M2k, MPTP2078-bushy, and TPTP v9.2.1, learned policies solve up to 46% more problems than leanCoP, and reach proofs in an order of magnitude fewer steps.

The Turing jump has no fixed point on the Turing degrees: $\mathbf a <_T \mathbf a'$ for every degree $\mathbf a$. After passing to the ideal completion, however, a natural fixed-point phenomenon appears. We study the Scott-continuous lifting $\Gamma:\operatorname{Idl}(\mathbf D_T)\to\operatorname{Idl}(\mathbf D_T)$, given by $\Gamma(I)=\downarrow\{\mathbf a':\mathbf a\in I\}$. Starting from the computable degree, Kleene iteration reaches its first fixed point at stage $\omega$, namely the Turing ideal of arithmetical degrees; more generally, above $\mathbf a$ the least fixed point is the ideal of degrees arithmetical in $\mathbf a$. To pass beyond this fixed point, we introduce a limit-uniformization operator. Although the ideal of finite jumps contains every $\mathbf 0^{(n)}$, it does not contain the uniform limit oracle $\mathbf 0^{(\omega)}=\deg_T\!\left(\bigoplus_{n < \omega}0^{(n)}\right)$. The uniformization operator adjoins this oracle only when all finite jump degrees are present. It is monotone but not Scott-continuous. Composing jump closure with one such gate yields closure ordinal $\omega\cdot 2$; gates at $\omega,2\omega,3\omega,\ldots$ yield closure ordinal $\omega^2$. Thus non-uniform closure under relativized halting problems is Scott-continuous and reaches fixed ideals, while uniform coding of an entire prior hierarchy is infinitary, discontinuous, and reopens diagonalization. This gives a domain-theoretic semantics for the successor/limit distinction in transfinite Turing-jump hierarchies and links failures of Scott continuity with closure ordinals.

We introduce spatio-temporal polyhedral reachability logics, extending dynamic topological logic with polyhedral semantics and a path-based spatial reachability operator. Formulas are interpreted over polyhedra, with admissible valuations ranging over polyhedral subsets; the spatial modality is interpreted as interior, the binary operator $\gamma(\varphi,\psi)$ expresses reachability of a $\psi$-point through a $\varphi$-region, and the temporal modalities are interpreted by a PL-homeomorphism and its inverse. We define h-dynamic reachability spaces and axiomatize the corresponding h-dynamic extensions of the known reachability logics of topological, finite, Alexandroff, and polyhedral spaces. The main result is soundness and completeness for the intended classes of invertible dynamical systems.

Formal theorem proving enables machine-verifiable evaluation of mathematical reasoning, yet existing benchmarks often emphasize aggregate proof accuracy, concentrate on a narrow range of mathematics, and provide limited evidence of robustness to equivalent reformulations. We introduce MathAdv, a diagnostic benchmark spanning 13 domains across undergraduate- and graduate-level mathematics. Alongside Lean 4 theorem proving, MathAdv provides up to three auxiliary tasks: multiple-choice questions that probe mathematical knowledge, fill-in-the-blank problems that isolate informal reasoning, and expert-crafted transformations that test robustness to problem presentation. Our evaluation of contemporary theorem provers yields four findings: formalization remains a major bottleneck; performance varies substantially across mathematical domains; natural-language guidance helps general-purpose LLMs but can hinder proof-specialized models; and mathematically equivalent reformulations expose substantial robustness limitations. Together, these results show how component-wise evaluation can reveal model capabilities and failure modes that aggregate theorem-proving accuracy obscures. The dataset and evaluation scripts are available at https://github.com/margotyjx/MathAdv.git.

The Job Shop Scheduling Problem with Power Requirements (JSPPR) extends the classical job shop scheduling problem by imposing time-varying limits on instantaneous power consumption. Previous studies have used a mixed-integer linear programming formulation and the GRASP x ELS metaheuristic, but no SAT-based exact approach or constraint programming model has been reported. This paper develops the first exact SAT and constraint programming (CP) formulations for the JSPPR. On the 35 published benchmark instances, both SAT and CP prove global optimality for all instances and obtain identical optimal makespans, substantially improving upon the best previously reported results. They also establish four improved makespan values over the GRASP x ELS results reported in the original study. CP proves optimality faster than SAT, while both exact approaches substantially improve the optimality coverage of the MILP formulations, which prove optimality on only 6 and 10 instances using CPLEX and Gurobi, respectively. The certified optimal solutions also reveal inconsistencies in several previously reported benchmark results, including makespans below the proven optimum. We provide corrected optimal makespans and a complete set of certified optimal results for the JSPPR benchmark, establishing a reliable reference for future studies.

Mixed-Integer Linear Programming (MILP) is a fundamental tool for combinatorial optimization with extensive real-world applications. A central challenge is designing computationally efficient MILP formulations. Large Language Models (LLMs) offer new opportunities to automate the modeling process, from deriving formulations to strengthening them. Reliable automation requires robust methods for verifying that proposed formulations preserve the underlying optimization problem. However, existing approaches evaluate formulations numerically and fail to reason about general problem instances. We resolve this limitation by introducing a constructive definition of MILP reformulation that can be formalized in Lean and machine-checked. We develop FLARE (Formulation-Level Automated Reformulation Evaluation), a method that uses an LLM-based agent and the Lean proof assistant to verify proposed reformulations against a reference formulation. To evaluate our approach, we introduce FormulationBench, a challenging dataset of 20 problems and 109 formulations. FLARE outperforms existing methods, with 100% accuracy on the NP-hard subset of FormulationBench. Furthermore, FLARE produces a machine-checkable certificate for every reformulation it accepts. For cases where formal guarantees are not necessary, we introduce FLARE-NL, a fast and cheap LLM proxy that matches FLARE's accuracy but produces no certificate. These methods enable reliable verification in automated optimization modeling.

Path abstraction originated as a technique for counterexample refinement in probabilistic model checking. Given a discrete-time Markov chain, it summarises the probabilities passing through a subset of the states onto new transitions of a smaller chain. In earlier work, we proved its correctness and that it is monotonically absorbing. In this paper, we extend path abstraction from reachability probabilities on discrete-time Markov chains to expected rewards on Markov reward models. Working in a novel free monoid view of Markov chains throughout, we prove that path abstraction preserves the Markov reward model structure when abstracting over arbitrary sets of states, and that it remains monotonically absorbing. Finally, we give a numerical recipe, accompanied by a reference implementation in PARI/GP, that computes path abstraction by solving linear equation systems. Its correctness rests on the relationship between expected rewards and expected visiting times of transitions.

Peak power limits restrict concurrent tasks and may increase assembly-line cycle time. To the best of our knowledge, this study is the first to minimize cycle time for the simple assembly line balancing problem type 2 (SALBP-2) with a fixed number of workstations and a fixed limit on total instantaneous power. An exact satisfiability (SAT) method finds feasible schedules, searches systematically for shorter cycles, and proves optimality when possible. Two reproducible formulas define looser and tighter power limits for 72 cases based on the standard SALBP library, with Gurobi and CPLEX providing commercial MIP and CP comparisons. Relative to standard SALBP-2 optima, the two limits increase the best-known cycle time by 16.49% and 61.02% on average. The best-performing SAT configurations find a feasible solution for every case, solve more cases to optimality than each commercial solver, and when both prove optimality, are almost always faster under the reported settings.

Physical implementations of Turing Machines remain rare, and existing electromechanical demonstrators and mechanical logic games typically require manual operator intervention, either to trigger each computational step or to reconfigure the state table, or both. This restricts prior physical models to short, operator-paced demonstrations and prevents autonomous execution of extended computations. This paper addresses that gap with a hardware Turing Machine that enables autonomous multi-step execution and reprogrammable optical input without manual intervention between programs. The system integrates an Arduino Mega for state-transition logic, dual NEMA 17 stepper motors for bidirectional tape actuation, infrared reflectance sensors for symbol detection, and an ESP32-CAM-based optical punched-card reader for automated state-table loading. Hole detection under non-uniform illumination used a Breadth-First Search flood-fill algorithm with local adaptive thresholding rather than fixed global thresholding, driven by the memory and library constraints of the ESP32-CAM's microcontroller environment; this improved card-decoding accuracy from 75% to 90% (100% with mechanical card flattening) on a 20-card test set. Mechanical evaluation showed fabrication accuracy of +/-0.15 mm, rack-and-pinion positional error below 0.3 mm across 50 trials, and voltage supply stability within +/-0.2 V under full system load. End-to-end computation was validated against a parallel software simulator (tlang), with all hardware outputs matching the simulated reference exactly across multiple test programs. The system advances prior physical Turing Machine demonstrations through autonomous execution, reprogrammable optical input, and quantitative evaluation of its mechanical, optical, and computational performance.

Many problems in the verification of recursive programs can be reduced to pushdown model checking. In this problem, we are given as input a pushdown automaton (PDA) over a constant-sized stack alphabet, and a description of undesirable behaviors given by an intersection of NFAs, and the problem is to decide if there is a behavior of the PDA that belongs to the set of undesirable behaviors. It is well-known that there is an algorithm for this problem that runs in time $O(n^{2k} |\Sigma| + n^{3k})$, where $n$ is the maximum number of states of the PDA and the NFAs, $\Sigma$ is the common input alphabet, and $k-1$ is the number of NFAs. Despite the importance of this problem, no better algorithm is known for it. In this paper, we provide an explanation for this lack of progress using the lens of fine-grained complexity theory. We prove that if the $3k$-Clique hypothesis (resp. combinatorial $3k$-Clique hypothesis) is true, then for any $\epsilon > 0$, there is no algorithm (resp. combinatorial algorithm) that solves this problem in time $O((n^{(\omega-1)k} |\Sigma| + n^{\omega k})^{1-\epsilon})$ (resp. $O((n^{2k} |\Sigma| + n^{3k})^{1-\epsilon})$) where $\omega$ is the matrix multiplication exponent. Furthermore, using the combinatorial hypothesis, we also show that pushdown model checking over constant-sized input alphabets cannot be solved in time faster than $O(n^{3(k-1)-\epsilon})$ for any $\epsilon > 0$. Finally, we investigate the possibility of an $O(N^{3k-\epsilon})$ time algorithm for this problem where $N$ is the total bit size of the input. We formulate a new hypothesis, the 2NPDA$(k)$ hypothesis, that helps explain the lack of $O(N^{3k-\epsilon})$ time algorithms for this problem. To corroborate this hypothesis, we show a web of linear-time reductions between the 2NPDA$(k)$ hypothesis, pushdown model checking, and other problems in formal language and automata theory.

Control invariance validates that dynamical systems have a control input that preserves a given property at all times. This paper introduces a set of sound axioms and proof rules in differential dynamic logic (dL) that enable verification of control invariance. First, the scalar and vector comparison principles, relating a system of differential equations to a comparison system such that invariance properties can be established more easily, are axiomatized in dL. This axiomatization primarily utilizes differential ghosts, which are proof-theoretic generalizations of comparison systems. Next, with the comparison principles serving as the basis, comparison invariants are introduced, and sound axioms and proof rules are derived. Comparison invariants reduce the question of control invariance to a functional inequality on its Lie derivative for a suitable class of functions, moreover, the right choice of function can result in decidable arithmetic. Furthermore, the perennially popular control barrier functions (CBFs) used in safety-critical control are shown to be a special instance of comparison invariants. This yields an axiomatization of CBFs that leads to a dedicated set of proof rules. The rules allow for the verification of CBFs, which are traditionally used for synthesizing safe controllers without verification. Lastly, comparison invariants are shown to unify several other safety verification techniques, including Darboux invariants and differential invariants, further cementing their versatility.

For multiplicatively independent natural numbers $\alpha$ and $\beta$, Villemaire showed in 1992 that the first-order theory of Presburger arithmetic expanded with both Büchi predicates $V_\alpha$ and $V_\beta$ is undecidable, as it encodes multiplication. In recent years, Hieronymi and Schulz showed that Presburger arithmetic expanded with the weaker power predicates $\alpha^\mathbb{N} = \{\alpha^n: n \in \mathbb{N}\}$ and $\beta^\mathbb{N}$ is also undecidable, while Karimov et al. showed that the existential fragment of this theory is decidable. These results left open the natural problem of determining the decidability of the existential fragment of Villemaire's original expansion. We settle this question for coprime $\alpha$ and $\beta$. Specifically, we give a quantifier-elimination argument that proves the decidability of the existential fragment of $\mathsf{FO}(\mathbb{Z};<,+, V_\alpha, V_\beta)$.

We present QisMC, the first quantum model checker dedicated to debugging Qiskit programs. On the theoretical side, we introduce the notion of quantum-classical transition system and a quantum computation tree logic (qCTL) grounded in Birkhoff-von Neumann logic for modeling the behaviors and specifying the properties of Qiskit programs, respectively. On the implementation side, QisMC provides an end-to-end framework encompassing transition system generation, logical formula representation, and model checking algorithms, and it efficiently performs image computation based on decision diagrams. These methods and design principles give QisMC advantages over previous Qiskit program debuggers, including a unified property specification language, a fully automated and exhaustive verification process, and the ability to generate counterexamples. Extensive illustrative examples and benchmark evaluations demonstrate the practicality, efficiency, and scalability of QisMC in verifying realistic quantum programs.

CSFLOC is a non-CDCL SAT decision procedure based on counting subsumed full-length ordered clauses. The classical CSFLOC loop traverses the ordered space of full-length clauses by a monotone counter: if the current full-length clause is not subsumed by the input formula, its negation is a satisfying assignment; otherwise, a subsuming clause determines a counter jump. The main bottleneck is the repeated search for such a subsuming clause. This paper presents CSFLOC-WL, and its current implementation CSFLOC-WL3, in which this search is replaced by watched-literal prefix propagation over the negation of the current full-length clause represented by the counter. The central mechanism is early conflict detection: if propagation under a common prefix derives opposite unit consequences for the same variable, then the two reason clauses are resolved immediately and the resolvent is used as a new counter-jump cause. The resulting solver is not a CDCL solver: it has no CDCL decision tree, no restart policy, and no first-UIP backjumping loop. It remains a counter-guided full-length-clause-counting solver, but it imports the watched-literal data structure and reason clauses as engineering tools for discovering jumps. Experiments on selected UNSAT SATLIB instances compare CSFLOC-WL3 with CSFLOC21TU and CaDiCaL 3.0.0. The results are mixed: CSFLOC-WL3 is strong on several random 3-SAT instances near the random-3-SAT satisfiability threshold, whereas CSFLOC21TU remains faster on several structured cases, apparently because it contains a more mature cache mechanism that is not yet present in CSFLOC-WL3.

We construct the category of overt discrete quasi-Polish spaces and the category of compact Hausdorff quasi-Polish spaces (and some of their subcategories) as internal categories of the category of effective quasi-Polish spaces and computable maps. To demonstrate that the constructions are natural, we show that Stone duality is computable, in the sense that the dual contravariant functors and the natural transformations demonstrating their adjointness are computable.

Large Language Models (LLMs) do not natively track the path of exclusions that a coherent discourse demands. When an input rests on a fabricated authority, a misapplied mechanism, or a surreptitious analogy, an unsteered LLM tends to engage with it as if it were well-posed, and this affects its generation. POLANYI++, an LLM-steering method that uses heuristics, ontologies and problem-solving methods for tacit-knowledge extraction, produces an Extended Knowledge Graph (XKG) in OWL2, but when a sophisticated nonsensical input is reified into the graph alongside the legitimate triples, it gets hardly detectable by automated reasoners, since the XKG is generated jointly with the wrong assumptions. We introduce DARKSIDE, a coherence-auditing method on top of POLANYI++. DARKSIDE formalises an explicit data structure of accumulated exclusions over discourse time, complemented by a warrant axis that classifies each named referent as Warranted, Unattested, Misattributed or Fabricated. The method is anchored in nine theoretical fragments unified under a shared deep frame of path integrity. The resulting DARKPOLANYI is evaluated as a steering layer over Gemini 3 on BSBench, a 100-item adversarial corpus of sophisticated-sounding nonsense across multiple domains, with Claude Sonnet 4.6 as an independent judge. DARKPOLANYI scores 1.89/2 mean versus 0.95/2 for the unsteered Gemini 3 Pro baseline; on the 97 cases with valid judgments in both arms, paired McNemar gives a paired bootstrap mean-diff = +0.92 (95% CI [+0.75, +1.08], p = 0.0001). The evidence supports an architectural claim: when an LLM forward pass is wrapped in an ontology-mediated auditing, structurally inevitable hallucination can be partially recovered. The XKG functions as the missing memory that LLMs lack, and the warrant axis as an epistemic firewall.

Linear-time temporal properties, such as those described by Linear-time Temporal Logic, are typically modelled as sets of infinite traces. Yet, in a run-time verification context, such as when testing or monitoring a system, only a finite prefix of the system's behaviour can be observed. For some properties, these finite prefixes may be definitive—a yes or no answer can be given without further observation. By enriching the semantics of LTL with these definitive prefixes, we give a proper inductive accounting of the semantics of LTL$_3$, a multi-valued variant of Linear-time Temporal Logic for run-time verification applications. The semantic descriptions of LTL$_3$ in previous work are given only in terms of their relationship to conventional LTL. We show that the semantics of LTL and of LTL$_3$ are isomorphic. In addition, we formalise the formula progression evaluation technique, popularly used in runtime verification contexts, and show its soundness and completeness up to finite traces with respect to our semantics. Then, we turn to linear-time properties more generally: using our theory of definitive prefixes, we re-prove the well-known safety-liveness decomposition theorem, and reconstruct the topology of infinite traces. We define monitorability for properties, providing neat topological characterisations for various monitorability classes, and arrange them into a hierarchy. All of our definitions and proofs are mechanised in Isabelle/HOL.

Similar to Skolem's nonstandard models of Peano's naturals, we show that axiomatic semantics based on Hoare logic has nonstandard models and so does not specify a unique, well-defined, and formal operational semantics of programming languages. We propose to enrich axiomatic semantics with additional proof obligations to solve this ambiguity problem. These proof obligations are always satisfied for standard trace models so that Hoare logic proofs are unchanged for these standard models.

We develop a resource representation for step recursion in which mutable-state width and recursion descent are explicit and independent parameters. A width bound $u$ controls the size of the encoded machine state, while an effective descent $\rho$ determines the available recursion depth $\delta_\rho(u)$. For generalized-inverse descents, we derive the depth directly from generator growth and characterize the increasing sequences that can occur as generator orbits. We then connect this depth–width geometry to standard finite-branching computation. Every deterministic bounded-state dynamics is realizable by a single ordinary bounded step recursion over a fixed finite numerical basis. Using deterministic, existential, universal, or alternating aggregation on the same local dynamics yields the corresponding machine semantics. After closure under the width reparameterizations needed to absorb fixed local cost, the resulting language classes are exactly the machine time–space classes on profiles $(\delta_\rho(u),u)$. Finally, profile domination quotients effective descents by admissible width reparameterization. Some depth curves collapse, yet polynomial widths support an explicit infinite strict hierarchy between the canonical polynomial- and exponential-depth profiles. Thus descent remains a nonredundant resource coordinate after polynomial width reparameterization; standard complexity classes are calibration points.

Weighted model counting (WMC) and probabilistic model checking (PMC) are two well- established frameworks that are independently developed, the former for probabilistic inference, the latter traditionally for probabilistic verification, though recently also applied to inference. The formal relationship between the two frameworks, however, remains largely unexplored. In this paper, we lay the foundations for how they relate: we present (1) a mapping from cycle- free parametric Markov chains (pMCs) to arithmetic circuits (ACs), enabling the reduction of reachability probability computations in such pMCs to a weighted model counting problem on the corresponding ACs, and (2) a mapping from a subclass of arithmetic circuits – with probabilistic semantics – back to parametric Markov chains. We propose a detailed correspondence between the entities of WMC and PMC, and discuss how our mappings enable transferring optimization techniques such as bisimulation minimization across the frameworks.

Whether large language models (LLMs) can perform the abductive leap from evidence to a new system of axioms, commonly referred to as a jump, has recently attracted considerable debate. A prominent position holds that LLMs are structurally incapable of such jumps, while recent studies challenge both its mechanism and empirical evidence. One of the main reasons why the debate remains open is the difficulty of defining the jump precisely enough to test it. In this paper, we attempt to develop a formal account of the jump in four steps and measure the second. These steps ask what the default completion of partial data is, when the constraints exclude it, whether the new structure agrees with later observations, and how successive jumps compound. We define a jump instance as a finite extension problem whose constraints exclude the canonical completions given by the Kan extensions and leave one correct completion up to renaming. In this setting, a model with a canonical default performs the second step by producing the correct completion under the constraints. We evaluate fourteen models across three certified families. The canonical completion returns once in $13{,}300$ constrained answers across all runs. Several calibrated models also give the correct completion reliably, including three API models that solve $159$ of $162$ primary chain trials, suggesting that they can jump at this step. We further formalize the third and fourth steps, whose empirical evaluation remains future work. We hope our work paves the path for formalizing and measuring the full jump in the future. The code of the paper is available at https://github.com/EEthanShi/kan-jump-test.

Verification and validation (V&V) are crucial methods for evaluating the requirements and specifications of dynamical models that fulfill their intended purposes. Parallel Discrete EVent System Specification (PDEVS) is a system-theoretic modeling approach for creating modular, hierarchical component-based simulation models. In this paper, we introduce Constraint-DEVS, a method for creating bounded Parallel DEVS models that lend themselves, in addition to simulation, to model checking. We extend the DEVS-Suite framework to create Constraint-DEVS specifications which can then be model checked using a proposed state exploration protocol with the Parallel DEVS abstract simulator protocol. These capabilities, along with the support for non-determinism, complex data transfer, and performance-related property checking, make Constraint-DEVS and its accompanying DEVS-Suite a unique framework for the development, verification, and validation of discrete-event systems. In order to demonstrate this work, we developed and verified models of Network-on-Chip. Also, we detail behavioral design artifacts for the DEVS-Suite framework's hybrid model-checking and simulation engine.

We align three upper ontologies that sit under UK and NATO defence data infrastructure: the Information Exchange Standard (IES), the Higher Quality Data Model (HQDM) that underpins the National Digital Twin, and Basic Formal Ontology (BFO). No public alignment between IES and HQDM existed. Promoting a hand-curated 17-correspondence crosswalk to OWL and reasoning over the complete merged ontologies with HermiT produces three results that we believe matter beyond this pair.

A quantitative equational theory $U$ reasons about terms that agree up to a numerical error. It presents a free algebra $T_UA$ over a metric space $A$ of generators, the terms of the syntax at the least distance the axioms derive, and that metric is its semantic content. We give a functorial invariant of it, the persistent magnitude homology of $T_UA$: a barcode where the module is tame, finite linear algebra where $T_UA$ is finite, Lipschitz in each degree. Magnitude homology is graded by length and knows nothing of persistence, its persistent refinement nothing of where its bars begin and end, yet the two are one construction: filtering the length nerve by sublevel sets of the length yields the persistence module, and the associated graded of that filtration is the magnitude complex. A long exact sequence exchanges them, and each side gains what it lacked. Magnitude homology locates the critical values of the barcode, so a graded computation lists the lengths at which an endpoint can occur, and the barcode acquires a stability estimate of $(n+1)\delta$ in degree $n$ under a perturbation of size $\delta$, and a computed perturbation shows that the factor cannot be dropped. An inclusion of theories induces a morphism of the presenting monads and, where the induced map is bijective and shortens no distance by more than $\delta$, a comparison of barcodes under the same bound, so a barcode movement measures the metric-semantic strength of the added axioms. Four examples are computed, one in every degree.

The theory of Equality with Uninterpreted Functions (EUF) is fundamental to constraint solving and program verification. Uninterpreted functions abstract concrete implementations, enabling generalization and simplification of theorems and proofs. However, standard EUF restricts function composition to fixed finite depths (e.g., $f^k(x)$ where $k$ is constant). This work extends EUF to EUF$^n$, supporting parametric composition depth for unary functions (e.g., $f^n(x)$ where $n$ is a natural number variable). An EUF$^n$ formula can be viewed as a disjunction of infinitely many EUF formulas, each instantiated by an assignment of natural numbers. Its satisfiability is defined by the satisfiability of at least one such instantiated EUF formula. We establish the decidability of the EUF$^n$ satisfiability problem via a conditional congruence graph (CCG) algorithm. This approach generalizes the standard congruence closure procedure by maintaining conditional equivalence relations between terms. The algorithm reduces the satisfiability problem to deciding existential sentences in Presburger arithmetic with divisibility, which is a decidable problem, thereby yielding a decision procedure for the quantifier-free fragment of EUF$^n$ with a 2NEXPTIME complexity upper bound. The enhanced expressiveness of EUF$^n$ enables new applications: (1) Encoding a decidable subclass of interleaved Dyck reachability problems where existing over/under-approximations produce false positives/negatives, and (2) Encoding a new decidable subclass of uninterpreted program verification problems.

For sixty years, machine verification has been a major cost overhead, affordable only for exceptional artifacts. Here we report that generative AI inverts this relationship: at AI speed, machine verification is not only economical but essential to productivity — it is the incorruptible referee that lets one person safely direct autonomous machine work at scale. In five weeks, one researcher on consumer AI subscriptions directed a small fleet of AI agents from application code, through a verified compiler and executive, to a RISC-V processor taped out on a community silicon shuttle; no proof passed through human review, and no RTL was written by a human. The working discipline — the Salt method — rests on a proof kernel no hallucinated proof can pass: mathematical claims travel between agents as kernel-checked artifacts, and human attention is reserved for statements, designs, and rulings. Verification is stated link by link, from the Lean 4 kernel to SAT-checked equivalence at the silicon boundary. We publish the complete accounting: theorem provenance, a pre-registered token meter, floor-bounded human time, and an error ledger whose catch numbering runs to #256 — a monotone counter over the mathematics campaign's append-only flags ledger, maintained 2026-07-07 to 2026-07-20 (one number, #79, was never assigned; later catches are recorded un-numbered) — against zero incorrect proofs reaching the record.