ABSTRACT. Neuro-Symbolic Programming (NSP) treats learning-enabled systems as programs that compose symbolic control structure composed with learned neural primitives for perception and prediction. NSP offers a principled response to a central challenge for logic and formal methods in the age of machine learning: how to obtain trustworthy, compositional behavior when key components are statistical and uncertain. This talk gives an gives an overview of recent advances in NSP along three axes: (1) domain-specific languages targeting real-world use cases, (2) learning techniques for fitting program structure based on informal specifications, and (3) approaches for ensuring correctness despite noisy neural components and incomplete specifications.

ABSTRACT. Coercion-resistance (CR) is a crucial security property in e-voting systems. It ensures that an attacker cannot compel a voter to vote in a specific way by using threats or rewards. The Loki e-voting protocol, proposed by Giustolisi \emph{et al.} at IEEE S\&P (2024), introduces a novel design that mitigates last-minute coercion through a re-voting mechanism. It also aims to address the usability issues of the seminal JCJ e-voting protocol, specifically: i) the requirement that voters can store and hide pre-agreed credentials, and ii) the ability of voters to convincingly lie while being coerced. In this work, we identify two vulnerabilities in Loki. The first is a brute-force attack that compromises the integrity of the evasion strategy. Specifically, this attack allows an adversary to cast a ballot on behalf of their victim in a way that the evasion strategy cannot defend against, rendering it ineffective. The second vulnerability is a forced abstention attack, which allows an adversary to detect when their victim has complied with their instruction not to vote. We generalise the integrity attack to reveal a fundamental dilemma: without pre-agreed secret credentials, it is not possible to prevent last-minute coercion. Finally, we show how reverting to pre-agreed secret credentials fixes the aforementioned vulnerabilities and discuss the trade-off between tallying efficiency and stronger trust assumptions.

ABSTRACT. Anonymous communication is essential for secure and private interactions over public networks. Existing solutions that provide provable anonymity rely on the so-called simple I/O setting, where every participant sends and receives the same number of messages, masking their true communication pattern. The only known way to enforce this setting is through dialing protocols. Such protocols establish pairwise conversations, but each recipient inevitably learns who attempted to contact them, violating sender anonymity, the guaranty that even the recipient cannot determine who attempted to contact them. In this work, we introduce the notion of enhanced dialing protocols, a broad class of protocols that enforce the simple I/O setting. We also initiate the first formal study of such protocols with respect to sender anonymity. We introduce a framework that captures three key properties: security, correctness, and fairness. Within this framework, we present Fusion, a protocol that achieves perfect correctness and fairness while incurring only unavoidable leakage, and Fusion+, a differentially private variant that reduces this leakage at the cost of some correctness. Through theoretical analysis, we quantify the fundamental trade-off between privacy and correctness in Fusion+.

ABSTRACT. Electronic voting aims to guarantee the same security properties than traditional paper-based voting, namely vote privacy and verifiability. While the formal verification of security protocols is now a mature filed with several powerful tools such as ProVerif or Tamarin, verifying voting protocols still pushes existing tools at their limits. We present in this work a proof framework for ProVerif that models an extensible election setting with an unbounded number of concurrent elections, voters and votes. We also develop a library of lemmas to aid the automatic verification. Crucially, the framework allows to reuse the same protocol model for both privacy and verifiability proofs. We apply the framework to several protocols of the literature and industry, showing the flexibility and applicability of our framework.

ABSTRACT. Maintaining a decentralized system requires a collective governance mechanism that allows the participants to agree on possible changes to the system. In particular, the governance mechanism should offer a voting functionality that allows the casting, collection, and tallying of votes in a confidential yet verifiable manner. Scaling this functionality for many millions of participants in a cost-effective manner is a critical requirement for permissionless blockchains that is currently still unmet. We put forward a ``layer-2'' approach to meet this requirement in the setting where a permissionless blockchain acts as the fall back ``layer-1'' mechanism. Specifically the key to our approach to scalability is that the protocol is realized in layer-2 fashion, i.e., the bulk part of the protocol is executed off-chain, but additionally secured on the blockchain with a minimal footprint. We prove our protocol secure in the universal composability (UC) framework. First, we formalize a governance ideal functionality $F_{L2Gov}$. Our definition offers high levels of confidentiality and verifiability. Moreover, in case of misbehavior, it is designed to allow attribution of faults so that appropriate action (such as slashing of on-chain funds) can be taken. Second, we demonstrate that our protocol UC-realizes the $F_{L2Gov}$ functionality based on a blockchain, an off-chain bulletin-board, a distributed homomorphic encryption functionality ($F_{DHE}$), and a number of other standard hybrids. To the best of our knowledge, this work presents the first blockchain layer-2 voting protocol with a rigorous security analysis. We also point out some challenges that arise when applying the UC framework to layer-2 protocols.

ABSTRACT. We introduce BlindReview, an anonymous and end-to-end verifiable peer review system that cryptographically guarantees both privacy and auditability through-out the reviewing process. We formally define these security properties and provide rigorous proofs that BlindReview satisfies them. We also present an implementation demonstrating our protocol’s practicality. This work serves as a foundation for verifiable and privacy-preserving peer review, offering a concrete solution to enhance transparency and reduce bias in the academic peer review process.

ABSTRACT. Neural network verification is active and rapidly maturing research area, with a growing ecosystem of solvers and tools. The VNN-LIB standard was introduced to support interoperability in this ecosystem, but Version 1.0 has several serious short-comings as a formal foundation: it lacks a precise syntax, semantics, and type system, offers limited expressivity, and relies on externally defined ONNX models whose semantics are informal and constantly evolving. The latter distinguishes VNN-LIB from established standards such as SMT-LIB, where queries are self-contained and have fixed semantics. In this paper we address these challenges by developing the theoretical foundations of VNN-LIB 2.0. Our key contribution is the introduction of the notion of a network theory, which abstractly characterises the minimal semantic interface required from a neural network model format. This abstraction enables VNN-LIB to be defined independently of any specific ONNX version while remaining compatible with evolving model representations. Building on this foundation, we present a formal syntax for a more expressive query language, a type system for it over the numeric domains provided by the network theory, and finally a formal semantics. To ensure internal consistency, the standard is mechanised in the Agda theorem prover. VNN-LIB 2.0 therefore provides robust and rigorous foundations for trustworthy neural network verification.

ABSTRACT. Formal verification is paramount for neural networks in safetycritical domains yet remains constrained by the trade-off between precision and scalability, especially with modern high frequency activation functions. However, the inherent NP-hardness of the problem forces a fundamental trade-off between scalability and precision in existing methods, which fail to adequately capture the high-frequency nonlinearities of modern activations. To address this, Quadratic Approximation based Verification via Fourier series and Taylor truncation (QAV-FT) is proposed as a framework unifying Fourier-enhanced quadratic approximation and Taylor remainder aware error control. Specifically: (i) A Fourierbased quadratic abstraction is formulated for arbitrary activations, with a rigorous error bound established via Jackson’s theorem and Lebesgue constant analysis; (ii) A second-order propagation scheme utilizing Lagrange remainder theory is devised to analytically derive sound, tight bounds with reduced symbolic complexity; and (iii) These mechanisms are integrated into a scalable full-network verification algorithm. Empirical results on MNIST-FC and other benchmarks demonstrate that QAV-FT achieves an average certification accuracy of 96.8% across complex activations like Swish, GELU, and Mish, with favorable accuracy and efficiency over comparable methods on partial models.

ABSTRACT. Research on neural network verification has traditionally emphasized scalability. However, recent invalidations of formally verified neural networks highlight soundness as an equally important goal. Pursuing inherent soundness, we present Rocq-NN-Roll, the first verified prover for real-valued piecewise-affine neural networks. Rocq-NN-Roll combines a network and its specification into a piecewise-affine function and reduces the verification task to solving linear inequalities over each polyhedral region. Verified in Rocq, it also provides the first automated proof support for neural networks in any interactive theorem prover, highlighting their still underexplored role in this field.

ABSTRACT. Formal verification of Semantic Segmentation Networks is challenging due to high-dimensional output spaces and cumulative over-approximation errors in deep architectures. Existing verification methods based on specific Star-set reachability suffer from either exponential state explosion (exact splitting) or excessive conservativeness (interval-based relaxation). In this work, we present ATKVerifier, a verification framework for SSNs operating on an abstract domain named constrained-star (C-star), which captures spatial dependencies within MaxPool receptive fields through explicit predicate constraints. Our framework features: (1) an adaptive top-K lower bound mechanism that dynamically encodes K potential maximizers based on layer depth and interval overlap, balancing precision and computational cost through parameter-free adaptation; (2) an adaptive affine upper bound exploiting linear relationships between top candidates to replace conservative constant bounds; (3) region-level completeness (RLC), a spatial robustness metric quantifying the integrity of verified contiguous object regions. Experiments on M2NIST with three SSN architectures (16~24 layers) demonstrate 8~25% improvement in robust IoU over the state-of-the-art tool NNV, with the improvement scaling with the network's depth. For the 24-layer architecture, ATKVerifier achieves 59.2% RLC versus 43.8% of NNV, certifying 35.2% more complete semantic objects.

ABSTRACT. Formal verification of transformers has become increasingly important due to their widespread deployment in safety-critical applications. Compared to classic neural networks, the inferences of transformers involve highly complex computations, such as dot products in self-attention layers, rendering their verification extremely difficult. Existing approaches explored over-approximation methods by constructing convex constraints to bound the output ranges of transformers, which can achieve high efficiency. However, they may sacrifice verification precision, and consequently introduce significant approximation error that leads to frequent occurrences of false alarms. In this paper, we propose a transformer verification approach that can achieve improved precision. At the core of our approach is a novel usage of ReLU, by which we represent a precise but non-linear bound for dot products such that we can further exploit the rich body of literature for convex relaxation of ReLU to derive precise bounds. We extend two classic approaches to the context of transformers, a rule-based one and an optimization-based one, resulting in two new frameworks for efficient and precise verification. We evaluate our approaches on different model architectures and robustness properties derived from two datasets about sentiment analysis, and compare with the state-of-the-art baseline approach. Compared to the baseline, our approach can achieve significant precision improvement for most of the verification tasks with acceptable compromise of efficiency, which demonstrates the effectiveness of our approach.

ABSTRACT. Decision tree ensembles (DTE) are a popular model for a wide range of AI classification tasks, used in multiple safety critical domains, and hence verifying properties on these models has been an active topic of study over the last decade. One such verification question is the problem of sensitivity, which asks, given a DTE, whether a small change in subset of features can lead to misclassification of the input. In this work, our focus is to build a quantitative notion of sensitivity, tailored to DTEs, by discretizing the input space of the model and enumerating the regions which are susceptible to sensitivity. We propose a novel algorithmic technique that can perform this computation efficiently, within a certified error and confidence bound. Our approach is based on encoding the problem as an algebraic decision diagram (ADD), and further splitting it into subproblems that can be solved efficiently and make the computation compositional and scalable. We evaluate the performance of our technique over benchmarks of varying size in terms of number of trees and depth, comparing it against the performance of model counters over the same problem encoding. Experimental results show that our tool XCount achieves significant speedup over other approaches and can scale well with the increasing sizes of the ensembles.

ABSTRACT. Shielding is a prominent model-based technique to ensure safety of autonomous agents. Classical shielding aims to ensure that some- thing bad never happens and comes with strong guarantees about safety and maximal permissiveness. However, shielding systems for probabilistic safety, where something bad can happen, but only with an acceptable probability, has proven more intricate. This paper presents a formal framework that conservatively extends classical shields to probabilistic safety. In this framework, we demonstrate the impossibility to preserve the strong guarantees, provide natural shields with weaker guarantees, and offline and online shield constructions that provide strong safety guarantees. The empirical evaluation highlights the practical advantage of the new shields as well as computational feasibility.

ABSTRACT. Large Language Models perform well at natural language interpretation and reasoning, but their inherent stochasticity limits their adoption in regulated industries like finance and healthcare that operate under strict policies. To address this limitation, we launched Automated Reasoning checks (ARc): a public service that (1) uses LLMs with optional human guidance to formalize natural language policies, allowing fine-grained control of the formalization process, and (2) uses inference-time autoformalization to validate logical correctness of natural language statements against those policies. When correctness is paramount, we perform multiple redundant formalization steps at inference time, checking the formalizations for semantic equivalence. Our benchmarks show that ARc exceeds 99% soundness and achieves a near-zero false positive rate in identifying logical validity. Our approach produces auditable artifacts that substantiate the verification outcomes and can be used to improve the original text. ARc is the first commercial offering from a major cloud provider to integrate automated reasoning into a generative AI guardrail.

ABSTRACT. Modal logics extend classical first-order logic with the modalities of necessity (□) and possibility (♢). A model of a set of modal logic formulae can be represented by a Kripke structure. This paper describes a method and implementation for finding finite Kripke models for formulae in first-order modal logics. The approach relies on translating the modal logic formulae to classical logic formulae, using an SMT solver to generate a finite model of the classical logic formulae, then translating the classical model to a finite Kripke model. This process has been implemented in the new model finding system MoMo, which produces TPTP-compliant Kripke model representations. An evaluation on the modal logic problems in the TPTP problem library confirms the practicality of this approach. Up to the authors' knowledge, MoMo is the first model finder for first-order modal logics.

ABSTRACT. Program synthesis is the task of automatically deriving a program that has been specified by a user in advance. Combining automated theorem proving with program synthesis enables the automated construction of proven-to-be-correct programs, thereby ensuring software reliability. In this paper, we consider the superposition-based calculus extended to support synthesis of recursion-free programs allowing reasoning with uncomputable symbols. We present cases where the calculus fails and refine it to solve them. We prove that the refined calculus is sound. Finally, we also prove completeness in the following sense: if at least one computable program satisfying the given specification exists, we show that the modified calculus finds one.

ABSTRACT. Certificates are machine-checkable witnesses that help increase confidence in verification results by providing independently verifiable evidence beyond a simple yes/no answer. In this short paper, we present two certificate checkers for hardware model checking, Certifaiger and Cerbtora, which target bit-level and word-level verification of hardware designs, respectively. Certifaiger has been adopted in recent editions of the Hardware Model Checking Competition, but not described in the literature before. Cerbtora extends the same theoretical framework to the word level, in which certificates are expressed in the same modeling language as the design under test and are validated using efficient automated reasoning engines. We describe the architecture and main components of both tools and evaluate them on competition benchmarks.

ABSTRACT. This paper introduces Pgeon, a meta-prover framework that generates tableau-based automated theorem provers from declarative specifications. In Pgeon, the syntax of a given calculus, its tableau inference rules, and the proof-search strategy are described in a small domain-specific language that closely follows textbook presentations. From such a specification, Pgeon instantiates a fully functional prover, handling tableau construction, rule instantiation, branching, and backtracking in a logic-agnostic manner. Proof-search is driven by a strategy engine that gives users explicit control over exploration order while keeping logical content separate from operational concerns. Pgeon supports first-order reasoning through binders, capture-avoiding substitution, and extensible term generators required for Skolemization and free variable introduction. We describe the design of the specification language, the execution model of the tool, and the strategy mechanism, and illustrate the approach on case studies covering classical and intuitionistic propositional calculi and classical first-order tableau calculi.

ABSTRACT. Verifying existing software is hard: they are developed in languages notamenable to verification, they involve complicated optimizations that obscure the underlying logic, and they are gigantic in size. In this paper, we propose a way to ease this pain via a simplification framework that employs interaction trees as a language-agnostic interface. We show that local variable lifting, the technique underlying AutoCorres for the Simpl language, can be generalized to interaction trees via an implementation in Rocq (formerly Coq). A key challenge with simplifying interaction trees is that they are too dynamic to be pattern-matched on. We address this challenge via metaprogramming. Our metaprogramming framework is semi-automatic and proof-guided, i.e., we obtain the simplified code via a constructive proof of equivalence that can be automated via proof tactics, by utilizing Rocq's Derive extension. This approach gives us simplified code and the equivalence theorem in one step. We demonstrate that our approach is practical using examples inspired by real-world applications.

ABSTRACT. Craig's Interpolation theorem has a wide range of applications, from mathematical logic to computer science. Proof-theoretical techniques for establishing interpolation usually follow a method first introduced by Maehara for the Sequent Calculus and then adapted by Prawitz to Natural Deduction. The result can be strengthened to a proof-relevant version, taking proof terms into account: this was first established by Čubrić in the simply-typed lambda-calculus with sums and more recently extended to linear, classical and intuitionistic sequent calculi. In the present paper, we give a new proof of Čubrić's proof-relevant interpolation theorem by building on principles of bidirectional typing, and formalise it in the Rocq proof assistant.

ABSTRACT. Blockchains rely on economic incentives to ensure secure and decentralised operation, making incentive compatibility a core design concern. However, protocols are rarely deployed in isolation. Applications interact with the underlying consensus and network layers, and multiple protocols may run concurrently on the same chain. These interactions give rise to complex incentive dynamics that traditional, isolated analyses often fail to capture. We propose the first compositional game-theoretic framework for blockchain protocols. Our model represents blockchain protocols as interacting games across the application, network, and consensus layers. It enables formal reasoning about incentive compatibility under composition by introducing two key abstractions: the cross-layer game, which models how strategies in one layer influence others, and cross-application composition, which captures how application protocols interact concurrently through shared infrastructure. We illustrate our framework through case studies on Hashed Timelock Contracts (HTLCs) and Layer-2 protocols showing how compositional analysis reveals new subtle incentive vulnerabilities and supports modular security proofs. Also, by introduction of a novel rational miner model, we derive new conditions for the robustness of timelocks to bribing attacks.

ABSTRACT. Post-quantum cryptography has become pivotal for ensuring communication security in the quantum era. NTRU-based signature schemes have gained attention due to their computational efficiency and compact public keys and signatures, which reduce communication overheads. However, the algebraic structure of NTRU lattices introduces vulnerabilities in physical attack scenarios, where partial secret key leakage can severely undermine system security. In this paper, we propose the Dimension-and-Sample Reduced NTRU Attack (DSRNA). The core principle of DSRNA is to apply a dimension-reduction strategy that transforms the NTRU instance into a lower-dimensional NTRU instance with fewer samples, which is efficiently solvable via lattice basis reduction. Furthermore, we design a unified hint-embedding technique that jointly exploits side information from both secret keys f and g, thereby improving both attack efficiency and success rates. We evaluate the residual security of Falcon and its variants Hawk, under perfect, modular and approximate leakage models. Experimental results demonstrate security degradation. Compared to the method of May et al. at Asiacrypt 2023, DSRNA achieves speedups of 5.8X for Falcon-512 with 400 leaked coefficients and over 29.4X for Falcon-1024 with 905 coefficients. This study reveals the potential vulnerability of NTRU-based signature schemes to partial secret key leakage.

ABSTRACT. In IEEE CSF '18, Fischlin and Mazaheri introduced the notion of self-guarding cryptographic protocols as a countermeasure to algorithm substitution attacks. After a trusted initialization phase, a Self-Guarder wraps the user's cryptographic algorithm implementation and sanitizes it in a way that (1) prevents that an adversary can exploit the subverted implementation to exfiltrate user's data and (2) maintain the correctness of the genuine implementation. Whilst the proposed solutions in CSF '18 support a bounded number of executions before requiring a re-initialization phase, we show a universal self-guarder supporting an unbounded number of executions from a single trusted setup. Our self-guarder can be applied to any cryptographic primitive and any two-party computation protocol with the aid of a verifiable-computation-enabling compiler.

ABSTRACT. A secret sharing scheme is a cryptographic primitive that allows a dealer to share a secret among a set of parties, so that only authorized subsets of them can recover it. The access structure of the scheme is the family of authorized subsets. In a weighted threshold secret sharing scheme, each party is assigned a weight according to its importance, and the authorized subsets are those in which the sum of their weights is at least the threshold value. For these access structures, Beimel and Weinreb [IPL 2006] presented the best general constructions: The scheme with computational security has a total share size polynomial in $n$, while the scheme with perfect security has a total share size $n^{O(\log n)}$. However, these constructions require the use of shallow monotone sorting networks, which limits their practical use. In this work, we revisit weighted threshold secret sharing from a circuit-based perspective. By considering alternative circuits and formulas that avoid monotone sorting networks, we obtain substantial improvements in two directions. First, in the computational setting, we provide a computational scheme that is feasible in practice. Assuming the existence of one-way functions with security parameter $\lambda$, we show that any weighted threshold access structure over $n$ parties with threshold $\sigma$ admits a computational secret sharing scheme with share size $\lambda$, public information of size $O(\lambda n^2 \log \sigma)$, and a reconstruction procedure in which any authorized subset needs to download only $O(\lambda n \log \sigma)$ bits of public information. Notably, for weight distributions that arise in the most widely deployed blockchain networks, our construction reduces the total share size ranging from $300\times$ to $6700\times$ compared to the best previously known schemes. Second, extending these techniques, we obtain improved information-theoretic ramp weighted threshold secret sharing schemes. For any weights, threshold $\sigma$, and $\epsilon < 1$, we construct a $(\sigma,(1+\epsilon)\sigma)$-ramp weighted threshold scheme with share size $O\left((n/\epsilon) \log n\right)$, reducing the share size with respect to the state-of-the-art solutions.

ABSTRACT. Sequential functions are computable functions that admit no asymptotic speedup, even in the presence of massive parallel computational resources. Although extensively studied within complexity theory, they have received less attention in cryptographic applications. This situation changed with the recent introduction of \emph{verifiable delay functions}, which found practical use in decentralized cryptographic payment systems and renewed the practical interest in sequential functions. In particular, the closely-related notion of \emph{time-lock puzzles} (TLP), in which a secret can be recovered only after a prescribed amount of sequential computation, have re-emerged as a fundamental primitive. Post-quantum secure TLPs based solely on standard cryptographic assumptions are unknown. A relaxed variant -- TLPs with preprocessing, which allow for an expensive setup phase -- can be obtained using randomized encodings and the existence of worst-case non-parallelizing languages (NPL). In this work, we introduce a new post-quantum secure TLP with preprocessing. Our construction combines (i) cryptographic evaluation over encrypted data with (ii) a well-studied average-case hardness assumption in graph theory: refuting cliques in Erd\H{o}s--R\'enyi graphs using (resolution-based) proof systems. Sequentiality is proven by relating this task to the problem of deciding, in quasipolynomial time, whether an Erd\H{o}s--R\'enyi graph contains a planted clique of appropriate size. Building on a result of Atserias, Bonacina, de Rezende, Lauria, Nordstr\"om, and Razborov, which shows that clique refutation requires at least $n^{\Omega(k)}$ steps -- where $n$ denotes the number of vertices and $k$ is related to the clique size -- we identify clique refutation as a natural candidate for sequential computation. Moreover, such refutation proofs can be equivalently represented as read-once branching programs of comparable depth. Leveraging this correspondence, we construct a time-lock puzzle in which the clique refutation instance is not revealed in the clear, but instead encrypted using an \emph{attribute-based encryption} scheme. This approach securely encodes the graph structure while allowing holders of appropriate attribute-keys to evaluate the branching program. To ensure efficiency, we require attribute-based encryption schemes whose parameter growth is logarithmic in the size of the evaluated function; existing constructions are known to satisfy this requirement.

ABSTRACT. In the context of the Equational Theories Project, Terence Tao posed the challenge of finding alternatives to a complicated 62-step proof found by the Vampire superposition prover. We introduce a proof minimization tool called Krympa. Using a combination of brute force and heuristics, and exploiting both Vampire and the Twee equational prover, the tool reduces the 62-step proof to 20 steps, each corresponding to a rewrite. In an empirical evaluation, it also performs well on 1431 equational problems originating from the same project, reducing in particular a 151-step proof to only 10 steps.

ABSTRACT. We address generating theorems from a given set of axioms, without proof goal, aiming at value from a mathematical point of view or as lemmas for automated proving. As benchmark, we convert a fragment of the Metamath database set.mm. Our techniques are centered on proof terms and condensed detachment. This ties in with automated first-order proving by proof structure enumeration, and links to Metamath and formulas-as-types. Our methods for generating theorems are based on partitioning the set of proof terms into inductively characterized levels. We study two ideas for improvement: Lemma synthesis by DAG compression of proof term sets, and incorporating combinators into proof terms. Our lemmas significantly improve solution rates of provers, e.g., of Vampire from 74% to 94%, and of leanCoP from 7% to 44%.

ABSTRACT. Lifting Boolean-reasoning techniques to the SMT level most often requires producing theory lemmas that rule out theory-inconsistent truth assignments. With standard SMT solving, it is common to "lazily" generate such lemmas on demand during the search. With some harder SMT-level tasks ---such as unsat-core extraction, MaxSMT, T-OBDD or T-SDD compilation--- it may be beneficial or even necessary to "eagerly" pre-compute all the needed theory lemmas upfront. Whereas in principle "classic" eager SMT encodings could do the job, they are specific for very few and easy theories, they do not comply with theory combination, and may produce lots of unnecessary lemmas. In this paper, we present theory-agnostic methods for enumerating complete sets of theory lemmas tailored to a given formula. Starting from AllSMT as a baseline approach, we propose several improved lemma-enumeration techniques, including divide&conquer, projected enumeration, and theory-driven partitioning, which are highly parallelizable and which may drastically improve scalability. An experimental evaluation demonstrates that these techniques significantly enhance efficiency and enable the method to scale to substantially more complex instances.

ABSTRACT. This paper presents a novel extension of the superposition calculus for reasoning about formulas in Separation Logic (SL). Our approach integrates the efficiency of saturation-based theorem proving with the expressive power of SL, which is widely used to describe and reason about memory heaps. The target logic strictly extends first-order equational logic with SL constructs built from points-to atoms and separating conjunctions. The resulting calculus retains the core strengths of the superposition paradigm while addressing the distinctive semantic challenges of SL. We prove that the calculus is sound and complete with respect to the standard redundancy criterion.

ABSTRACT. Several successful strategies in automated reasoning rely on human-supplied guidance about which term or clause shapes are interesting. In this paper we aim to discover interesting term shapes automatically. Specifically, we discover abstractions : term patterns that occur over and over again in relevant proofs. We present our tool Twitch which discovers abstractions with the help of Stitch, a tool originally developed for discovering reusable library functions in program synthesis tasks. Twitch can produce abstractions in two ways: (1) from a partial, failed proof of a conjecture; (2) from successful proofs of other theorems in the same domain. We have also extended Twee, an equational theorem prover, to use these abstractions. We evaluate Twitch on a set of unit equality (UEQ) problems from TPTP, and show that it can prove 12 rating-1 problems as well as yielding significant speed-ups on many other problems.

ABSTRACT. Let ${\cal T}$ be a theory allowing a form of elimination of existential quantifiers (possibly for formulae in a certain class). We analyze possibilities of constructing (most general) solutions w.r.t.\ ${\cal T}$ for formulae of the form $\exists x_1, \dots, \exists x_n \phi(x_1, \dots, x_n, y_1, \dots, y_m)$, where $\phi$ is a quantifier-free conjunction of literals in the signature of ${\cal T}$, and the free variables $y_1, \dots, y_m$ are regarded as parameters. We show that in the presence of function symbols which describe "{\sf if}-{\sf then}-{\sf else}" constructions in certain models of ${\cal T}$, we can describe the most general solution of such formulae, thus generalizing results about the existence of most general unifiers in discriminator varieties. We illustrate the ideas on examples.

ABSTRACT. Interactive theorem provers (ITPs) are promising tools for ensuring program correctness, but users often complain about their poor usability and steep learning curve. A common complaint, especially among new users, are confusing error messages that expose details of the ITP's underlying theory or implementation details. In this work, we investigate how adding hints to three types of scope and type checking error messages in the Agda ITP affects the new users' debugging experience. We evaluate the effectiveness and perceived helpfulness of those error messages by conducting a between-subjects user study where we provide a series of Agda code snippets, each containing a single error that the participants have to fix based on the error message. We measure the success rate, time taken to fix the error, and perceived helpfulness for each code snippet with the original as well as the enhanced error message and determine the statistical significance of adding the hint. Our results show that correct hints can improve the success rate and time taken to fix the error, and that error messages with hints are rated significantly more helpful than those without. Additionally, we find that while error messages with incorrect hints are often rated as more misleading, they do not significantly impact the success rate or time taken to fix the error. These results show that adding hints to error messages is a viable step on the path towards making ITPs more widely accessible.

ABSTRACT. Intermediate Verification Languages (IVLs) play the same role in verification as Intermediate Representations in compilation, a layer that separates a verifier's language-specific front-end from its logic automation back-end. Successful IVL tools such as Boogie, Why3, and Viper generate Verification Conditions (VCs) that are sent to an SMT solver. The verifier output can be trusted only if these VCs are sound with respect to the formal semantics of the IVL. Formalizing the semantics of IVLs and verifying the soundness of corresponding VC Generators with respect to this semantics is challenging if one wants to model realistic features of IVLs such as mutually recursive definitions, lexical variable and contol-flow labeled scopes, interpreted and uninterpreted functions, and unbounded loops. B3 is a new IVL. This paper presents a formalization of B3's semantics, a VC Generator for the language, and a soundness proof that these two correspond. All three components are authored in the Dafny programming language and verifier. The key theoretical contribution of this work is a methodology to split the IVL's semantic encodings into two layers of abstraction to cover realistic aspects of the semantics, while keeping the proofs amenable to automation. Optimized for Dafny-style automation, the first layer is used to verify the soundness of the VC Generator procedure. Optimized for expressiveness, the second layer is used to capture the semantics in a natural way.

ABSTRACT. We benchmark four proof assistants (Agda, Idris 2, \lean and \rocq) through a single test suite. We focus our benchmarks on the basic features that all systems based on a similar foundations (dependent type theory) have in common. We do this by creating an ``over language'' in which to express all the information we need to be able to output correct and idiomatic syntax for each of our targets. Our benchmarks further focus on ``basic engineering'' of these systems: how do they handle long identifiers, long lines, large records, large data declarations, and so on. Our benchmarks reveals both flaws and successes in all systems. We give a thorough analysis of the results. We also detail the design of our extensible system. It is designed so that additional tests and additional system versions can easily be added. A side effect of this work is a better understanding of the common abstract syntactic structures of all four systems.

ABSTRACT. We introduce a generic certificate format for verifying liveness properties in hardware model checking, relying purely on propositional predicates and not involving explicit counters. Our certificates can be efficiently validated via a fixed number of SAT checks. The proposed format is compatible with state-of-the-art liveness checking algorithms. We present certificate generation for several representative techniques, including rLive, liveness-to-safety reduction, and k-liveness, as well as for a preprocessing method based on stabilizing constraint extraction. Experimental results on benchmarks from the Hardware Model Checking Competition demonstrate that our approach is practically effective with very low certification overhead, and our certificate checker was able to successfully validate all certificates that were generated.

ABSTRACT. Whenever automated provers such as automatic software verifiers deliver a verdict (true or false), they are expected to produce also a witness that justifies the verdict. This allows independent validation of the verdict using the witness by a third party, increasing trust in the results. The current standard exchange formats for witnesses in software verification do not support program termination. To fill this gap, we propose an extension of the witness format that is based on transition invariants as a general and effective formalism. We justify this by (a) proving that transition invariants can encode other popular termination arguments like ranking functions and (b) providing three different validation approaches for transition invariants, which together can validate most of the exported witnesses. Our approach based on transition invariants was integrated into version 2.1 of the recently released witness format, and the software-verification community has adopted the format for SV-COMP.

ABSTRACT. KoAT is a tool to automatically infer complexity bounds and prove termination of (possibly recursive) integer programs. To this end, KoAT implements an alternating modular inference of upper runtime and size bounds for program parts. In particular, KoAT uses a portfolio of different techniques to analyze subprograms. The power of our approach is demonstrated by an extensive experimental evaluation.

ABSTRACT. Verifying stateful software systems remains challenging due to complex control structures and intricate state interactions, often necessitating pre-existing behavioral models. We introduce Seal, an abstract interpreter that automatically derives sound and precise symbolic finite automata models. In tests on real-world applications, Seal generates sound and precise automata within minutes and, when employed in dynamic model checking, uncovers fifteen previously unknown bugs. These findings demonstrate that our approach can effectively connect code to model-based verification for stateful software systems.

ABSTRACT. We study the fully automated amortised cost analysis of purely functional data structures like skew heaps, as well as weight- and rank-biased leftist heaps. For that we generalise earlier works on automated amortised resource analysis by developing a type inference based approach based on a generic type system. This allows for modular reasoning and the inference of precise and optimal cost bounds. More specifically, we extend the work on the ATLAS system by Leutgeb et al., which was developed to cover the analysis of splay trees and some closely related data structures. To enable the analysis of skew heaps, however, and the even more challenging (amortized) analysis of leftist heaps, we have developed a range of new techniques for type-based automated analysis. By introducing a generic type system we allow for arbitrary (classes of) potential functions, compared to the use of hard-coded potential functions in ATLAS, which we have implemented in Haskell in an entirely modular way. We have also greatly enhanced the existing type inference algorithm by extensions in multiple directions, including path-sensitive reasoning, data structure invariants, and template parameters for piecewise defined potential functions. We show how our newly developed system supports the use of all known potential functions for analyzing skew heaps and leftists heaps, confirming the known bounds.

ABSTRACT. In numeric-intensive computations, it is well known that the execution of floating point programs is imprecise as floating point arithmetic incurs round-off errors. Although round-off errors are small for a single floating point operation, the aggregation of such errors may be dramatic and cause catastrophic program failures. Therefore, to ensure the correctness of floating point programs, round-off error needs to be carefully taken into account. In this work, we consider polynomial invariant generation for floating point programs, aiming at generating tight invariants under the perturbation of round-off errors. Our contribution is a novel framework for applying polynomial constraint solving to address the invariant generation problem, which is also the first polynomial constraint solving based approach that handles floating point errors to our best knowledge. In our framework, we propose a novel combination of round-off error analysis and polynomial constraint solving, aiming to circumvent the cost of handling a large number of error variables in the floating point model. Experimental results over a variety of challenging benchmarks show that our framework outperforms SOTA approaches in both time efficiency and the precision of generated invariants.

ABSTRACT. We present a parallel abstract interpretation technique for polynomial programs with assertions presented as unions of range bound constraints. We use the powerset domain of hyper-rectangles to over-approximate sets of reachable states. Our key technical contributions include novel abstract transformers and refinement operators that account for the semantics of polynomial assignments and guards more precisely than earlier work, while remaining amenable to parallelization and efficient implementation. This is achieved by appealing to Farkas' Lemma and Handelman's Theorem, and by exploiting geometric properties of unions of hyper-rectangles. Our abstract interpretation technique proves safety properties of many polynomial programs that state-of-the-art abstract interpretation tools fail to prove. We have implemented our approach in a tool called PolyAbs, and experimentally evaluated it on a suite of benchmarks. Our experiments demonstrate the improved precision and broader coverage of PolyAbs vis-a-vis state-of-the-art abstract interpretation tools, including a commercial-grade tool.

ABSTRACT. Several extensions of Datalog perform probabilistic inference by allowing users to annotate input facts and rules with probabilities. While extremely useful in many domains (e.g., quantitative program analysis), existing systems typically do not support incremental inference, meaning that even small changes trigger costly recomputation from scratch. This paper presents PINQ, the first incremental solving framework for probabilistic Datalog. Given a previously solved program and a set of changes, PINQ updates query probabilities by reusing the old derivation graphs and compiled decision diagrams. The key idea is to translate structural changes into parametric updates whenever sound to avoid redundant recomputation. Our framework combines an incremental derivation graph construction algorithm with an adaptive BDD construction technique that safely reuses existing BDDs via weight calibration whenever possible. Experimentally, PINQ achieves an average speedup of 17X over recomputation from scratch on a representative set of program analysis benchmarks.

ABSTRACT. Reference counting bugs in Linux kernel drivers can lead to severe resource mismanagement and security vulnerabilities. We intro- duce DrvHorn, a novel automated tool to detect these bugs by reducing reference counting verification to an assertion checking problem leverag- ing the Linux driver interface. Through efficient modeling of the Linux kernel and aggressive program slicing, DrvHorn discovered 545 bugs, of which 424 were previously unknown, across all platform drivers in v6.6 Linux kernel, with a lower false positive rate of 29.9% compared to prior studies. To address the root causes of these newly discovered bugs, we submitted patches to the Linux kernel, and 45 of them were merged.

ABSTRACT. As privacy concerns rise, numerous laws require machine learning-based applications to comply with stringent privacy regulations. While Homomorphic Encryption (HE) allows computation directly on encrypted data, existing HE-based inference solutions suffer from significant computational and memory overhead for both single and multiple samples. Additionally, current methods require many rotation keys, which limits their practicality in a broader range of scenarios. To address these challenges, we propose channel-interleaved packing (CIP) to embed three-dimensional (3-D) data into 2-D ciphertexts, enabling 3-D HE convolution to be performed as a 2-D HE convolution combined with channel aggregations via ciphertext rotations, thereby significantly reducing the number of rotation keys required. To further improve the performance of CIP-based convolution, we introduce an efficient 2-D convolution that halves the number of HE multiplications. For computationally intensive inference tasks, we employ partial-kernel and mini-batch strategies that iteratively process sliced kernels and subsets of samples, aggregating the results to produce the final output. Experimental results demonstrate the superior efficiency of our method compared to the state-of-the-art HE-based approaches by Lee et al. (ICML’22) and Cheon et al. (IEEE TDSC’24) in both single-sample and multi-sample scenarios. Using ResNet18 and VGG16 with a batch size of 64, our solution achieves speedups of up to 2.9× and 4.6×, respectively. When processing a single test sample, the speedups increase to 4.4× and 27×. Moreover, our method requires only 29 rotation keys for evaluation, which is at least 35% fewer than previous works, resulting in an overall memory reduction of approximately 50%.

ABSTRACT. Randomized smoothing has become essential for achieving certified adversarial robustness in machine learning models. However, current methods primarily use isotropic noise distributions that are uniform across all data dimensions, such as image pixels, limiting the effectiveness of robustness certification by ignoring the heterogeneity of inputs and data dimensions. To address this limitation, we propose UCAN: a novel technique that \underline{U}niversally \underline{C}ertifies adversarial robustness with \underline{A}nisotropic \underline{N}oise. UCAN is designed to enhance any existing randomized smoothing method, transforming it from symmetric (isotropic) to asymmetric (anisotropic) noise distributions, thereby offering a more tailored defense against adversarial attacks. Our theoretical framework is versatile, supporting a wide array of noise distributions for certified robustness in different $\ell_p$-norms and applicable to any arbitrary classifier by guaranteeing the classifier's prediction over perturbed inputs with provable robustness bounds through tailored noise injection. Additionally, we develop a novel framework equipped with three exemplary noise parameter generators (NPGs) to optimally fine-tune the anisotropic noise parameters for different data dimensions, allowing for pursuing different levels of robustness enhancements in practice.

ABSTRACT. Differentially Private Stochastic Gradient Descent (DP-SGD) is a cornerstone technique for ensuring privacy in deep learning, widely used in both training from scratch and fine-tuning large-scale language models. While DP-SGD predominantly relies on the Gaussian mechanism, the Laplace mechanism remains underutilized due to its reliance on $\ell_1$ norm clipping. This constraint severely limits its practicality in high-dimensional models because the $\ell_1$ norm of an $n$-dimensional gradient can be up to sqrt{n} times larger than its $\ell_2$ norm. As a result, the required noise scale—and thus the privacy loss—grows significantly with model size, leading to poor utility or untrainable models. In this work, we introduce LAP$_2$, a new solution that enables $\ell_2$ clipping for Laplace DP-SGD while preserving strong privacy guarantees. We overcome the dimensionality-driven clipping barrier, by computing coordinate-wise moment bounds and applying majorization theory to construct a tight, data-independent upper bound over the full model. By exploiting the Schur-convexity of the moment accountant function, we aggregate these bounds using a carefully designed majorization set that respects the $\ell_2$ clipping constraint. This yields a multivariate privacy accountant that scales gracefully with model dimension and enables the use of thousands of moments. Empirical evaluations demonstrate that our approach significantly improves the performance of Laplace DP-SGD, achieving results comparable to or better than Gaussian DP-SGD under strong privacy constraints. For instance, fine-tuning RoBERTa-base (125M parameters) on SST-2 achieves 87.88% accuracy at $\epsilon$ = 0.54, outperforming Gaussian (87.16%) and standard Laplace (48.97%) under the same budget. On image classification, a CNN on MNIST achieves 93.29% accuracy at $\epsilon$ = 0.88 with LAP$_2$, compared to 96.08% (Gaussian) and only 16.44% (Laplace).

ABSTRACT. We present a variant of the multiset path order for untyped applicative term rewriting. Compared to existing work, our variant incorporates two distinctive features, dubbed arity assignment and reification, to overcome difficulties in handling partial and variable application.

ABSTRACT. We report on the new ARI infrastructure that supports tools and competitions in term rewriting. It offers ARI-COPS, a database for confluence problems and competition results, and ARIWeb, a convenient web interface for tools that participate in the annual confluence competition. These are built on top of the new ARI format for rewrite systems, a format converter, certifiers for competition results, and a duplicate checker.

ABSTRACT. This paper introduces the algebra normalizing tactic for the Lean theorem prover. This tactic expands on the existing ring tactic by additionally supporting a scalar multiplication action over a fixed commutative (semi)ring. It supports rational constants in the base ring even when the main ring is not a field, which lets us implement a suite of tactics for manipulating both univariate and multivariate polynomials. These features are implemented by adapting the existing implementation of ring while retaining support for variable exponents.

ABSTRACT. Vampire proves theorems completely automatically in first- and higher-order logic extended with theories. Proof checking is increasingly demanded to consolidate user trust in Vampire's output. We describe ongoing efforts in reconstructing Vampire proofs as trusted proofs in Lean.

ABSTRACT. The free-variable tableau method has been widely used in order to automate proofs in multiple kinds of logics. Many Automated Theorem Provers (ATPs) rely on this approach, either because it is the only available method (e.g., in certain modal logics) or because it facilitates the generation of proof certificates. However, as far as the authors know, its results have never been formalized in a proof assistant. In this paper, we present TableauxRocq, a deep-embedding of free-variable first-order tableaux in the Rocq prover. The formalized calculus is proved sound and provides a modular Skolemization system that enables the use of Skolemization-based optimisations. Moreover, we show how TableauxRocq can be used as a certifier for ATPs by adapting the Goeland prover to output proofs in the TableauxRocq format. By using the full power of reflection, thereby providing a fully certified proof checker for free, we show that the deep embedding performs at least as well as a shallow embedding, even without proof optimizations, and strictly better when Skolemization-related optimizations are present in the proof.

ABSTRACT. Real root isolation is a fundamental subroutine in computer algebra, with applications ranging from algebraic number arithmetic to solving polynomial systems. Modern implementations typically employ subdivision methods based on root counting via Descartes’ rule of signs. In contrast, most existing formally verified root isolation procedures rely on Sturm’s theorem for root counting, leading to a noticeable gap between practical implementations and formally verified approaches. We take an initial step toward efficient verified real root isolation by formally verifying two simple algorithms based on Descartes’ rule of signs: a classical bisection procedure and a Newton-accelerated variant. In this paper, we describe the algorithms and present formal proofs of termination, soundness, and completeness. Brief experiments show promising performance improvements over existing formally verified approaches in Isabelle/HOL.