Papers

With the growing deployment of machine learning models, formal guarantees of the robustness and fairness of these models have become increasingly important in safety-critical and legal-compliance settings. However, model parameters are often commercial secrets that cannot be disclosed to auditors or end users. To this end, we present PANDA, a scalable system that uses zero-knowledge proofs (ZKPs) to prove the robustness and fairness properties of a model without revealing its private parameters. PANDA is built on top of CROWN, an efficient robustness certification framework that is used in many state-of-the-art formal verification tools for neural networks. The core contribution of PANDA is a novel algorithm for proving linear relaxation bounds for non-linear activation layers, yielding simple, lightweight proofs. Remarkably, our system can generate proofs of local robustness for neural networks with more than 2.9M parameters in 5 minutes, and can verify them in 10 seconds. Prior ZKP-based robustness system rely on exponential-time algorithms that cannot scale to nontrivial networks. In contrast, PANDA scales polynomially in the number of neurons in a network, allowing us to support neural networks 4 orders of magnitude larger than previous approaches with significantly reduced prover overhead.

This paper captures and extends some of the core results from the tech memo "A New Semantics for Belief Revision in Simplicial Complexes". As such, we set out to explore the implementation of action models in the setting of simplicial semantics for modal logic. Such an idea is not entirely new to the literature, showing up in both "A simplicial complex model for dynamic epistemic logic to study distributed task computability" and "Knowledge and Simplicial Complexes". However, we will explore action models in a more general setting. In particular, we will allow for action models for simplicial models for belief, as in "A Semantics for Belief in Simplicial Complexes". This will let us incorporate the notion of belief revision, as developed in "Simplicial Semantics for Belief Revision", into these action models. Moreover, we explicitly connect action models in the simplicial setting to distributed protocols as defined in the textbook "Distributed Computing Through Combinatorial Topology". We conclude with some speculation on how we might interpret distributed protocols with revision.

Functional dependencies are an important and well-studied class of database constraints that correspond to a notion expressed by dependence atoms in team logic. In practice, data often contain errors, so in some cases it might be useful to allow the database to have a small number of tuples that violate the desired dependency. Väänänen (2017) studied the axiomatisation of a notion of approximate dependence that specifies for each dependence atom how much of the database can be disregarded. We demonstrate that the interaction of approximate dependence atoms is more complicated than previously thought in the sense that there is a semantic consequence that is not captured by the inference rules introduced before. We show that Väänänen's axiomatisation is still complete in the restricted case of unary dependencies. We also consider the complexity of model checking for approximate dependence: it is NP-complete for disjunctions of two atoms and LOGSPACE-hard for individual atoms.

Nearly a decade ago, Calude et al. showed that parity games can be solved in quasi-polynomial time. This result is now understood in terms of universal trees. By reduction to parity games, the quasi-polymonial result can benefit all omega-regular games. However, beyond such reductions, and with the exception of Rabin games, our understanding of the role of universal trees in direct solutions is still quite limited. In this work, we refute the common view that universal trees are relevant only for games that admit memoryless winning strategies. We contribute a full understanding of how universal trees interact with Zielonka trees for the solution of Streett and Emerson-Lei games. As a consequence, we show that winning regions and strategies in Streett games with $n$ vertices, $m$ edges, and $k$ pairs can be computed in time $O(mk\log(k)k!|U(n,k)|)$, where $U(n,k)$ is a universal tree for $n$ leaves and depth $k$. This improves upon the best previously known complexity result for Streett games, which relied on reduction to parity games and their quasi-polynomial solution. Furthermore, we show that winning regions and strategies for Emerson-Lei games with $n$ vertices, $m$ edges, and $c$ colors can be computed in time $O(mc\log(c)c!|U(n,c/2)|)$, again improving over reductions to parity games. Notably, our approach yields memory-optimal strategies, in contrast to those obtained via reductions to parity games. Finally, we show how universal trees can be used to bound the recursion tree of the Zielonka-McNaughton algorithm for Emerson-Lei games. This leads to a symbolic algorithm that replaces the factor $n^c$ in the time complexity of existing symbolic approaches with $|U(n,c)|$.

We settle an open question related to Tarski's High School Algebra problem by showing that no 11-element algebra can satisfy the High School Identities while refuting Wilkie's identity. We encode the search as a SAT instance and independently verify the result. As a byproduct, we obtain a new 12-element countermodel that is not isomorphic to the previously known one.

By Tarski's undefinability theorem, no consistent classical formal system that includes arithmetic can define its own truth predicate. Reflective Grounded Arithmetic (RGA) is a powerful arithmetic whose universal quantifier is grounded in its own reflected proof search, and whose paracompleteness circumvents Tarski's theorem. This paper presents a machine-checked Isabelle/HOL development that defines a truth predicate for RGA's full language, quantifiers included, as an internal term of RGA itself. This term is compiled from a primitive-recursive decider for its operational semantics, and proven adequate in both directions. Around this predicate the development closes a square of metatheorems: for every formula RGA proves, RGA derives the formula's internal truth; every grounded-true formula is internally provable; internal truth implies internal provability; and the consistency of RGA follows. The two directions run on disjoint internal machines—a certified decider and a certified proof-checker, both RGA terms. Reaching these results involved substantial ordinary reasoning carried out within RGA: coded syntax and substitution, compiled primitive-recursive functions with symbolic unfolding laws, internal strong induction, and a verified proof-checker for the system written in the system's own formal language. The development thus demonstrates along the way that RGA is a workable formal system supporting nontrivial mathematical reasoning.

Knowledge graphs modeled in RDF are powerful for describing static knowledge, but they cannot capture or reason about the dynamic behavior of physical systems, e.g., systems described by differential equations, which is a critical gap for AI-driven cyber-physical systems. To solve this, we propose RDFdL, a framework that integrates RDF with Differential Dynamic Logic (dL) to represent and reason about both static knowledge and the continuous dynamics of physical systems. For the dynamic part, we syntactically represent differential equations and ranges in the state space in RDF and SHACL and provide semantics using a translation to dL. Linking RDF and dL through their shared foundation in first-order logic achieves a unique integration: verification results for safety and reachability properties in the dynamic logic domain become available as entailment to SPARQL queries over RDF data. We implement the pipeline using Apache Jena for ontology-driven RDF reasoning and KeYmaera X, the theorem prover for dL, and sketch its applicability in manufacturing.

Software developers rely on packages to reuse existing functionality instead of implementing everything from scratch. Python developers commonly provide package and interpreter dependencies using configuration files, such as requirements.txt or setup.py. Package managers in Python, such as pip, can install packages according to dependency and interpreter version constraints specified in configuration files. However, Python dependency resolution remains challenging: (1) different packages may require incompatible versions of the same dependency; (2) dependencies may require a Python interpreter version that is incompatible with the interpreter used for the project, making a valid environment impossible; and (3) pip, the most popular Python package manager, resolves conflicts via backtracking, repeatedly trying candidate versions without knowing whether a valid execution environment exists or not. To address these challenges, we present SMTpip, an interpreter-aware environment inference technique for improving the executability of Python source-code artifacts. SMTpip constructs a dependency knowledge graph using metadata stored in the Python Package Index (PyPI) that hosts millions of package releases, encodes both package version constraints and interpreter compatibility constraints specified in configuration files into Satisfiability Modulo Theories (SMT) formulas. Solving these formulas identifies a set of package versions and an interpreter version that jointly satisfy all declared constraints. Empirical evaluation on multiple datasets from open-source Python projects shows that SMTpip achieves substantial speedups – $6.9\times$ over pip, $9.6\times$ over Conda, $3.2\times$ over smartPip, and $4\times$ over PyEGo – while consistently producing constraint-consistent environments.

We introduce monoidal su-categories, an abstract categorical notion of single-input higher-order process over a monoidal category. The definition separates a base category C of lower-order processes from a monoidal category V of holes or supermaps and axiomatizes the compatibility needed for partial application to bipartite processes. For a fixed monoidal base C, monoidal su-categories, monoidal su-functors, and monoidal su-natural transformations form a 2-category MonSuCatC. We then show that the category Optic[C] of coend optics is 2-initial in this 2-category, giving an alternative universal-property characterisation of coend optics as the minimal monoidal theory of single-hole contexts.

Solovay reducibility is studied intensively as a tool to compare the approximability and the degree of randomness of left-c.e. reals. By definition, a real is left-c.e. if it has a left-c.e. approximation, that is, it is the limit of an effective nondecreasing sequence of rationals. If reals $\alpha$ and $\beta$ have left-c.e. approximations $a_0, a_1, \ldots$ and $b_0, b_1, \ldots$, respectively, such that the approximation ratios \[ \frac{\alpha-a_n}{\beta-b_n} \] are bounded from above by a constant, the real $\alpha$ is Solovay reducible to $\beta$. The latter is the case for any such $\alpha$ and $\beta$ and their left-c.e. approximations whenever $\beta$ is Martin-Löf random by the Kučera-Slaman Theorem [DOI:10.1137/S0097539799357441]. This result was substantially strengthened by Barmpalias and Lewis-Pye [DOI:10.1016/j.jcss.2017.06.002], who demonstrated that, under the given assumptions, the approximation ratios are not only bounded but actually converge to a limit, which does not depend on the considered left-c.e. approximations. There is a quest for a suitable extension of Solovay reducibility to the class of all reals. Promising candidates include S2a-reducibility on the set of computably approximable reals by Zheng and Rettinger [DOI:10.1007/978-3-540-27798-9_39] and monotone Solovay reducibility by Titov [DOI:10.1007/978-3-031-95908-0_33]. For the latter, Titov [DOI:10.1017/jsl.2025.10157] demonstrated that the theorems of Kučera and Slaman and of Barmpalias and Lewis-Pye extend to all reals. He conjectured further [DOI:10.1017/jsl.2025.10157, Conjecture 3.2] that similar extensions hold for S2a-reducibility in terms of its functional characterization by Kumabe, Miyabe, and Suzuki [DOI:10.3233/COM-230486]. In this work, we refute this conjecture by proving that the analogue of the Barmpalias-Lewis-Pye Limit Theorem does not hold for S2a-reducibility.

In value-based argumentation, an audience's ordering of values decides which attacks succeed as defeats. In many settings the deciding factor is not the audience but the circumstances: the same attack may succeed at one procedural stage, or under one regulation, and fail at another. Context-dependent argumentation frameworks (CDAFs), a model we recently introduced, capture this directly: one attack relation and a defeat function that switches each attack on or off per context, so every context induces an ordinary Dung framework. This raises a reduction question: can one value assignment with per-context orderings reproduce the defeat function, collapsing the CDAF into a VAF? We present a polynomial-time decision procedure for this question and map the harder neighbouring problems, with upper bounds from NP to $\Sigma^p_3$. We also present a validated reference implementation and a measurement: representability is rare and falls fast with the number of contexts.

The development of models demands sound modeling and simulation knowledge as well as domain knowledge. Every model should accurately represent a system's dynamics and be verifiable. Toward this objective, this research introduces an agentic PDEVS-LLM framework to assist human modelers in generating and verifying PDEVS statecharts for behavior modeling of atomic Parallel Discrete Event System Specification (PDEVS) models. The framework supports (re)generating plausible facts from a system description prompt using the agentic LLM used for generating plausible facts. Inconsistencies in plausible facts lead to incorrect PDEVS statecharts having logical structure and behavioral inaccuracies. A controlled-correction mechanism is developed to verify the logical consistency of the plausible facts. The agentic LLM is used to generate key behavioral conditions from the system description prompt. The plausible facts are then verified against the behavioral conditions using propositional logic entailment for a finite number of times. The verification results enable the generation of modification prompts that can reduce errors in generated plausible facts, resulting in more accurate PDEVS statecharts. To verify a statechart's logical correctness, its Timed Automata counterpart is manually created and verified for deadlock and reachability properties. The human modeler may regenerate plausible facts and PDEVS statecharts iteratively and incrementally. A basic correctness metric is introduced to quantify the completeness and accuracy of the expected behavioral traits of the PDEVS statechart models. A collection of example systems with varying levels of complexity is developed to demonstrate the capabilities and limitations of LLMs. The evaluation of the proposed verification mechanism shows a substantial improvement in the logical consistency of generated statecharts.

We introduce the category $\mathbf{SSS}$ of sample-smooth spaces over a mixed site. The test objects are the products $\Omega_n := \mathbb{R}^n \times \Omega$ of a Cartesian space with the universal Hilbert cube $\Omega$ carrying all universally measurable sets, and a space is a set with a family of admissible plots $\Omega_n \to \mathcal{X}$ closed under precomposition. Smoothness and measurability are then not two structures glued along an axiom, but one structure over one site. The site has finite non-empty products, because $\Omega$ absorbs its own square; its Karoubi envelope contains every $\mathbb{R}^n$; and it has mixed morphisms $\omega \mapsto (W(\omega),\Phi(\omega))$, which turn measurability of a smooth family from an axiom into a consequence. $\mathbf{SSS}$ is a concrete quasitopos: complete, cocomplete, cartesian closed and locally cartesian closed, with a classifier for embeddings. Morphisms of Cartesian spaces are exactly the $C^\infty$ maps and manifolds embed full and faithfully, both without Boman's theorem. Every object has tangent and cotangent spaces, every morphism a differential. The modalities sit in an adjoint string $\Pi \dashv \flat \dashv \natural \dashv \sharp \dashv \Lambda$, making $\mathbf{SSS}$ cohesive over quasi-universal spaces. The point is the probability monad. Defining the plots of $\mathsf{P}(\mathcal{X})$ as push-forwards of $\mathcal{X}$-plots at every test object, $\mathsf{P}$ is an unconditional strong commutative affine monad on all of $\mathbf{SSS}$ – functor, unit, product of kernels, multiplication and the monad laws are each one line of seed splitting – and its Kleisli category, of differentiable simulators, is a Markov category. The reparametrisation trick holds by construction: every Kleisli morphism is plot-wise a sampler, stably under composition. A reflection theorem locates the whole gain in a single plot family.

Making language models solve constraint problems reliably often means having them translate the problem into a formal specification and delegating the search to a sound solver. But the translation is itself a language-model task, and an unfaithful translation makes the solver faithfully solve the wrong problem. Existing pipelines repair only translations that crash, returning the solver's error message and falling silent when the program runs but is wrong. We replace the error message with a proof: when the generated program is unsatisfiable, we extract a minimal unsatisfiable core over the model's own constraints and hand it back the exact set that cannot hold together, a leakage-free signal that localizes the fault. On a new benchmark of 77 problems with an exact oracle, translation to Answer Set Programming is faithful on six of seven domains and fails only on aggregate coverage scheduling, which concentrates the translation tax in one diagnosable pattern. A minimal core, rather than a bare error, is what stops a weaker model from fabricating solutions to infeasible problems, cutting fabrication from 79% to 7%. A strong chain-of-thought baseline meanwhile matches the symbolic route on accuracy, so the route's value is not accuracy but certificates and its refusal to fabricate.

We propose two novel approaches for using Counterexample-Guided Abstraction Refinement (CEGAR) in Quantified Boolean Formula (QBF) solvers. The first approach develops a recursive algorithm whose search is driven by CEGAR (rather than by DPLL). The second approach employs CEGAR as an additional learning technique in an existing DPLL-based QBF solver. Experimental evaluation of the implemented prototypes shows that the CEGAR-driven solver outperforms existing solvers on a number of families in the QBF-LIB and that the DPLL solver benefits from the additional type of learning. Thus this article opens two promising avenues in QBF: CEGAR-driven solvers as an alternative to existing approaches and a novel type of learning in DPLL.

This paper presents a first-order multimodal logic programming system called MMLP. The system accepts arbitrary formulas as both programs and queries, without restricting either side to Horn clauses or a separate goal grammar. Its declarative semantics is given independently by a Hilbert system for selected D, T, I, B, 4, and 5 modal principles. Execution uses a nested proof calculus with finite grammar certificates for modal propagation. Certificate reachability is equivalent to the associated Horn closure, certificate existence is decidable, and the calculus is cut-free complete. For quantified answer computation, we give a unification algorithm based on permission sets that controls eigenparameter scope. The algorithm always terminates and fails exactly when no admissible solution exists. A successful run returns a unifier that is itself admissible and through which all admissible solutions factor. Computed answers are declaratively correct, and each declaratively correct answer is an ordinary output instance of a computed answer. In proof search, MMLP admits syntactic focalization and a fair and complete enumeration of focused answers. It represents exactly the same answer substitutions as Nguyen's pure logical KDI4s5-MPROLOG on their common fragment, while admitting a strictly larger program and query language.

Algorithms based on the enumeration of implicit hitting sets find a growing number of applications, which include maximum satisfiability and model based diagnosis, among others. This paper exploits enumeration of implicit hitting sets in the context of Quantified Boolean Formulas (QBF). The paper starts by developing a simple algorithm for QBF with two levels of quantification, which is shown to relate with existing work on enumeration of implicit hitting sets, but also with recent work on QBF based on abstraction refinement. The paper then extends these ideas and develops a novel QBF algorithm, which generalizes the concept of enumeration of implicit hitting sets. Experimental results, obtained on representative problem instances, show that the novel algorithm is competitive with, and often outperforms, the state of the art in QBF solving.

Higher-Dimensional Automata (HDAs) provide a geometric model of true concurrency. While hereditary history-preserving (hhp) bisimilarity is the finest behavioural equivalence in van Glabbeek's spectrum, no modal logic has previously characterised it on HDAs. We introduce several new intermediate equivalences that sit strictly between ST- and hhp-bisimilarity. We show how separating similarity and subsumption of paths leads to a clean formulation of these equivalences, and we present a modal logic that characterises hhp-bisimilarity. Natural fragments characterise ST-bisimilarity and the intermediate notions.

The Shapes Constraint Language (SHACL) is a W3C recommendation to express syntactic constraints, called shapes, on RDF graphs. SHACL validators are used to test whether a given graph adheres to such a shape. However, RDF graphs often come with OWL ontologies, whose implicit knowledge needs to be taken into account. This is classically handled by first applying reasoning and then performing the constraint checking on the results, often using different technologies which makes the process inefficient and vulnerable for mistakes. To overcome this, we propose to internalise the OWL axioms in the SHACL constraints; we construct a rewriting which takes as input both shapes and an OWL EL$^-$ ontology – a fragment of OWL EL restricting the usage of existential restrictions – and produces SHACL constraints. This output can then be evaluated by any validator supporting SHACL core regardless of its reasoning support, while yielding the same results as the traditional approach. The implementation of our translation is evaluated both against applying state-of-the-art reasoners and validators consecutively, as against validators with built-in reasoning support. For our benchmark, we show that our approach is in general more efficient in finding violations compared to the sequential approach, thus providing a powerful tool which simplifies combining reasoning with validation.

How do we govern AI systems whose reasoning we cannot fully inspect? Governance does not require understanding a system's reasoning. It requires stating what the system is obliged, permitted, and forbidden to do, and checking whether it complied. I present an implementation of Reified Input/Output Logic, the formalism behind the DAPRECO knowledge base, in Wolfram Language: the core I/O axioms, obligations, permissions, constitutive norms, reified eventualities, and temporal operators. I then test whether GPT-4 can translate English legal statements into the formalism, and report the failures: hallucinated functions, omitted temporal scope, deviation from the formalism, and (in the worst cases) code that runs, reads plausibly, but silently encodes the wrong norm. A case study, an AI guard dog operating under a computational contract, shows how formalized rules can extend from a contract directly into the operational code of an embodied agent, producing symbolic, auditable justifications for its behaviour. I argue that computational law can be used as a governance tool and that a desirable goal would be to formalize the law that can and ought to be programmatically executable.

We give a machine-checked proof, in Lean 4, of the universal property of multicentered blowups: given a finite family $Z$ of closed subschemes of a scheme $X$, presented on each chart by ideals, there is a scheme $\Bl_Z X$ over $X$, terminal among $X$-schemes on which every member of the family becomes an effective Cartier divisor. To the best of our knowledge this is the first formalisation of blowups, single- or multicentered, in any theorem prover. The proof is organised around the universal property of the multicentered dilatation of a ring: the initial algebra in which a finite family of ideals becomes generated by non-zero-divisors. Existence and uniqueness of the dilatation are established locally, on affine charts, and every subsequent step of the construction, the base change along open immersions, the comparison isomorphisms on overlaps, the triple overlap maps, the cocycle identity, and the independence of the chosen presentation, is deduced from that single local property by uniqueness alone. We give the exact theorem statement as formalized, the proof architecture, and the main new mathematical ingredients, together with the corresponding Lean code.

We represent the modular enlargement of an executable model by a pushout of finite typed presentations. Adhesivity preserves the original model and recovers the shared interface, while chosen pushouts make linking functorial and coproducts describe parallel attachments. A semantic comparison gives a precise criterion for behavioral persistence. Effective linking also bounds conditional prefix complexity; under the stated canonicalization and invariance assumptions, attachment and extension codes yield the same profiles of loss against complexity, up to additive constants, and share an exact scalar envelope. The result separates syntax, semantics, ideal complexity, and concrete coding cost, and shows that a preference for modularity can arise only through restrictions on the permitted attachments.

This paper will give a definition of belief revision within simplicial semantics. Starting from the work presented in "A Semantics for Belief in Simplicial Complexes" as a baseline, this paper modifies the semantics for belief given there to allow atomic formulae to be assigned to nodes, not facets. Conceptually and philosophically, this version of the semantics is better suited if one wishes to interpret the nodes of a simplicial model of epistemic logic as a "perspective" assigned to a particular agent. If nodes are perspectives, it then follows that worlds, or the facets of a simplicial model, are composed themselves of perspectives. This allows us to say that two worlds are more similar, or "nearer", if they share more perspectives. With this conceptual notion of nearness in hand, two different formal presentations of revision are given. We conclude by exploring some conceptual pitfalls surrounding these definitions under iterated revision, and motivate a few potential solutions that involve giving the agents a "memory" of what has been announced so far.

AI agents are increasingly used for programming, but do not provide any guarantee on the correctness of generated code. Verified code generation, in which an agent produces both an implementation and a machine-checked proof of its specification, offers a stronger path toward trustworthy AI-generated software. Existing benchmarks in this direction either focus on individual functions or only evaluate proof generation with provided implementations. It is still an open question whether agents can make coherent implementation and proof choices across real multi-module codebases. To bridge this gap, we introduce Vero, the first benchmark to evaluate joint implementation and proof synthesis at the repository level. Vero contains 43 multi-module instances sourced from real-world repositories spanning Python, Dafny, Verus, and Coq, and covering diverse domains from cryptographic protocols to distributed systems. Each instance consists of a multi-module Lean 4 repository with predetermined API interfaces, manually curated formal specifications, and reference implementations, supporting both proof-only and code-and-proof evaluation modes. To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification or incorrectness of reference code, which surfaces and corrects latent code and specification errors during curation. We evaluate frontier coding-agent configurations with Lean toolchain access. The strongest agent fully solves only 27 of 43 instances and closes no specifications on the hardest repositories. Vero provides a concrete testbed for measuring progress toward repository-scale verified software synthesis, where current agents still fall short. We release the benchmark, curation pipeline, and evaluation harness at https://github.com/sunblaze-ucb/vero.

We give the first theoretical characterization, and the first algorithm, for continuous monitoring of a distributed Cyber-Physical System (CPS) against a dense-time temporal logic specification. A distributed CPS is composed of multiple agents, each with a local clock; these clocks drift from each other, so there is no well-defined global time. When monitoring such a system's output signal against a temporal logic specification, it is not evident how to interpret the temporal constraints of the formula, and what satisfaction means. Yet CPS designers, like control engineers, typically think of their system's operation in terms of global time. Most existing techniques for monitoring distributed systems work with discrete-time specifications not suitable for CPS, and/or require an explicit mapping of temporal constraints to local clocks. We introduce an algorithm that addresses the above challenges for a fragment of Signal Temporal Logic (STL) that still includes all temporal operators. It relies on a novel extension of satisfaction signals to this partially synchronous setting (where clocks drift), and an analysis of the geometry of multi-dimensional partially synchronous time. The algorithm returns the set of all possible global moments that can satisfy the specification. Knowledge of these possible global moments is important for debugging distributed hybrid control systems such as fleets of drones and electrical grids. We derive the worst-case complexity of the algorithm, and implement a sound approximation of it that experimentally illustrates effective monitoring, even in scenarios of up to 50 agents.

We address the use of large language models (LLMs) to help discover Isabelle proofs. An Isabelle build establishes that the submitted theory is accepted, but not that an LLM changed only what the developer authorised. We present CAPRI, a contract-aware repair workflow in which Isabelle checks the proof and an independent checker enforces a machine-readable edit contract. Prompts, proposals, candidate repositories, diagnostics, verdicts, and hashes are retained for audit. We evaluate five workflows on twelve failed proofs from four developments, with three replicates per task and condition, giving 180 runs and 138 valid repairs. Of 144 terminal candidates accepted by Isabelle, six had modified protected text; all arose in iterative workflows that could edit a complete theory. A proof-body-only interface produced 29/36 valid repairs and no contract violations, compared with 31/36 for the corresponding full-theory workflow. One-shot repair produced 22/36, while a later prospectively frozen iterative workflow produced 32/36; these figures compare complete workflows rather than individual mechanisms. A separate post hoc OpenRouter campaign found no improvement in the designated Luna comparisons. A Sol configuration with matched demonstrations produced 33/36 repairs, compared with 29/36 in the frozen OpenAI Responses condition, but the difference was not statistically significant in a one-sided exact McNemar test ($p=0.0625$).

Two graphs $G$ and $H$ are homomorphism indistinguishable over a graph class $\mathcal{F}$ if they admit the same number of homomorphisms from every graph in $\mathcal{F}$. A wide range of relaxations of graph isomorphism arise this way: isomorphism itself over the class of all graphs [Lovász, Acta Math. Hung. 1967], equivalence under the $k$-dimensional Weisfeiler-Leman algorithm over the graphs of treewidth $\leq k$ [Dvořák, J. Graph Theory 2010], and quantum isomorphism over planar graphs [Mančinska-Roberson, FOCS 2020]. Since the class $\mathcal{F}$ is typically infinite, it is not clear a priori whether homomorphism indistinguishability over $\mathcal{F}$ is decidable; for planar graphs it is undecidable. Every class for which decidability was previously known is sparse. We give the first decidability results for dense graph classes: We introduce the dense Weisfeiler-Leman algorithm that decides homomorphism indistinguishability over the class of graphs of cliquewidth $\leq k$, the dense counterpart of treewidth. This relation was not previously known to be decidable. The algorithm colors $k$-tuples of vertex subsets rather than $k$-tuples of vertices. Beyond the class of all graphs of cliquewidth $\leq k$, we prove a general meta-theorem: homomorphism indistinguishability over every $\mathsf{CMSO}_1$-definable graph class of bounded cliquewidth is decidable, in randomized exponential time. For classes of bounded linear cliquewidth the bound improves to $\mathsf{PSPACE}$, and we show this is tight by exhibiting such a class for which the problem is $\mathsf{PSPACE}$-complete. These are the first general algorithms for homomorphism indistinguishability over dense graph classes.

Basic matching logic is matching logic without definedness. Symbols are interpreted as set-valued operations, element variables denote singletons and are bound by $\exists$, and no connective uniformly internalizes totality. For basic matching logic without fixpoints over an arbitrary one-sorted finitary signature, we prove global completeness ($\Gamma\vDash\varphi$ iff $\Gamma\vdash\varphi$, for arbitrary, possibly infinite $\Gamma$) and, as a corollary, conservativity of the definedness extension. The proof localizes $\Gamma$ to a theory $\Delta_\Gamma$ and reduces semantic consequence and derivability to the same local relation: $\Gamma\vDash\varphi$ iff $\Delta_\Gamma\vDash_\text{loc}\varphi$ iff $\Gamma\vdash\varphi$. A double-cover construction establishes the semantic equivalence. Least fixpoints destroy effective axiomatizability. Over a signature with one unary and two binary symbols and no constants, validity is not recursively enumerable; hence no sound calculus with a recursively enumerable proof relation is even weakly complete, already for the empty theory and without definedness. The positive result is also sharp in the number of sorts. Global completeness fails with three sorts for a satisfiable $\Gamma$. Thus the completeness conjecture holds for one sort and fails in general. The negative results arise from sort flow, fixpoint effectivity, and, for hybrid logic, an obstruction to every well-founded calculus whose leaves are hypotheses or valid patterns and whose rules respect localization. This yields a matching-logic-independent dichotomy: the language with state variables bound by $\exists$ and $\forall$ over modalities of arbitrary arity is globally complete without nominals, while no calculus in that well-founded class is globally complete once nominals are added.

Probabilistic programs with nondeterminism model planning problems in which a strategy resolves the nondeterminism to optimize an expected outcome. We study the multiobjective setting, optimizing several outcomes at once along a Pareto front, and provide a deductive, program-level account of strategy synthesis. Its core is a multiobjective preexpectation transformer mapping a tuple of postexpectations to the set of simultaneously achievable values, an element of the convex Hoare powerdomain. It conservatively extends weakest preexpectations and lifts standard loop rules. We develop rules to synthesize witnessing strategies as mixed determinizations that randomize over non-probabilistic determinizations. We prove the transformer and synthesis rules sound against an operational MDP semantics, without requiring a finite state space: our approach can be seen as a symbolic approach - at program level - for multiobjective optimization over infinite MDPs. We demonstrate our machinery using various case studies.

We present global and local algorithms for solving systems of equations over Noetherian posets with a bottom element, a general setting underlying many verification problems. Our algorithms compute the solution of a selected variable by restricting exploration to those parts of the system required to determine its value. We achieve this by computing variable dependencies by means of dependency oracles. Oracles guide the exploration of the system and provide sound termination criteria for local fixed-point computation. A key advantage of our approach is its flexibility: oracles can be customized, composed, or over-approximated, offering a principled way to trade precision for performance without compromising correctness. We evaluate our solution against existing algorithms from the literature and show that our prototype implementation is competitive and often outperforms specialized solutions, while remaining simple and adaptable across diverse application domains.