ABSTRACT. Diffie-Hellman groups are commonly used in cryptographic protocols. While most state-of-the-art, symbolic protocol verifiers support them to some degree, they do not support all mathematical operations possible in these groups. In particular, they lack support for exponent addition, as these tools reason about terms using unification, which is undecidable in the theory describing all Diffie-Hellman operators. In this paper we approximate such a theory and propose a semi-decision procedure to determine whether a protocol, which may use all operations in such groups, satisfies user-defined properties. We implement this approach by extending the Tamarin prover to support the full Diffie-Hellman theory, including group element multiplication and hence addition of exponents. This is the first time a state-of-the-art tool can model and reason about such protocols. We illustrate our approach’s effectiveness with different case studies: ElGamal encryption and MQV. Using Tamarin, we prove security properties of ElGamal, and we rediscover known attacks on MQV.

ABSTRACT. In symbolic models, equational theories are used to model the algebraic primitives of cryptographic primitives. Automated verification tools however only handle limited classes of equational theories to avoid performance and termination issues. In particular associative and commutative (AC) symbols have often been problematic, although they are common, e.g., to model addition, multiplication, exclusive-or (XOR), multisets, etc. In this paper we extend the Tamarin prover to allow users to specify AC symbols as part of their user-defined equational theory. To avoid termination issues, we propose a novel property that bounds certain deduction chains. We use Tamarin’s deduction algorithm to verify whether this bound is indeed correct for a given equational theory, generalizing previous work. Moreover, our work allowed to identify that Tamarin’s built-in XOR used an optimization that may lead to incorrect results, and would have influenced our results as well. Simply disabling the optimization results in non-termination on a significant fraction of examples from the Tamarin repository. We therefore design a new constraint reduction rule that discards some redundant constructor chains, and prove its correctness. We illustrate the effectiveness and efficiency of our approach using different examples, including XOR, multisets, reencryption, Diffie-Hellman exponentiation, and distributed decryption. It turns out that our property holds for all these examples, and that, compared to Tamarin’s built-in support for XOR or multisets, our approach only incurs a small overhead on startup when checking the property, but otherwise has similar performance on most examples. Re-encryption and distributed decryption were previously out of scope, and our model for Diffie-Hellman exponentiation, albeit simpler than the built-in, allows for the exponentiation symbol to be reused in further equations, which is not allowed for the built-in one.

ABSTRACT. Network protocol fingerprinting is used to identify a protocol implementation by analyzing its input-output behavior. Traditionally, fingerprinting operates under a closed-world assumption, where models of all implementations are assumed to be available. However, this assumption is unrealistic in practice. When this assumption does not hold, fingerprinting results in numerous misclassifications without indicating that a model for an implementation is missing. Therefore, we introduce an open-world variant of the fingerprinting problem, where not all models are known in advance. We propose an incremental fingerprinting approach to solve the problem by combining active automata learning with closed-world fingerprinting. Our approach quickly determines whether the implementation under consideration matches an available model using fingerprinting and conformance checking. If no match is found, it learns a new model by exploiting the structure of available models. We prove the correctness of our approach and improvements in asymptotic complexity compared to naive baselines. Moreover, experimental results on a variety of protocols demonstrate a significant reduction in misclassifications and interactions with these black-boxes.

ABSTRACT. Security protocols are concurrent processes that communicate using cryptography to achieve various security properties. Their formal verification has been the subject of much research, which has led to a number of successful tools. Several of these tools use variants of the applied pi-calculus as an input language to model protocols, though the internal representation used for verification may vary. The translation from processes to their internal representation has received relatively little attention despite its important role in the soundness and efficiency of the security analyses. We consider this problem within the Squirrel prover framework, where processes are translated to so-called systems of actions, which serve as the basis for a logic-based verification technique. Intuitively, actions consist of groups of elementary instructions. We provide a general theory for grouping instructions in a way that preserves both indistinguishability and trace properties, and we instantiate it to obtain a new translation procedure for Squirrel. We have implemented our procedure as a replacement of the original (unsound) translation, demonstrating that it can serve as an almost drop-in replacement in existing case studies.

ABSTRACT. The Lightweight Directory Access Protocol (LDAP) plays a crucial role in modern enterprise infrastructure for centralized authentication and authorization, yet lacks comprehensive formal verification. We develop a formal model capturing LDAP and its most popular authentication mechanisms (Simple Bind, SASL PLAIN, SASL-CRAM-MD5, SASL SCRAM- SHA-256 and SASL SCRAM- SHA-256-PLUS ). We bridge the gap between this formal model and the most widely used implementation of the protocol, OpenLDAP, by monitoring it using the SpecMon framework. We instrument the cryptographic library to generate an event stream which SpecMon continuously checks for compliance with the model. We use Tamarin to prove authentication properties, which thus transfer to OpenLDAP.

ABSTRACT. Modern stream-based monitors collect detailed statistics of the runtime behavior of the system under observation. If the systems runs in a privacy-sensitive context, this poses the risk of disclosing sensitive information. Differential privacy is the state-of-the-art approach for protecting sensitive information, however, integrating it into runtime monitoring is challenging: temporal operators can cause individual input values to influence multiple outputs over time, leading to repeated disclosure of private information. We propose an approach that automatically enforces differential privacy in stream-based monitoring specifications by analyzing temporal dependencies and injecting carefully calibrated noise into the specification. To preserve the utility of the outputs, we identify strategically chosen positions in the specification for noise injection and leverage tree-based mechanisms to mitigate the accuracy loss caused by noise injected into aggregation operators. We demonstrate the practicality and effectiveness of our approach in a case study on monitoring public transportation usage.

ABSTRACT. This paper presents the first symbolic bounded model checking technique capable of verifying ∀+∃+-liveness hyperproperties (expressed in HyperLTL) over arbitrary (non-terminating) reactive systems. Previous bounded procedures for HyperLTL handled only safety hyperproperties or arbitrary properties over terminating systems. We implement our technique as HyperLasso, and our evaluation results show that it consistently outperforms the explicit-state complete model checker AutoHyper (the only existing tool capable of automatically verifying this class of problems) at several complex bug-finding and synthesis problems.

ABSTRACT. We show how to use passive automata learning to infer models of attacker-defender interactions in cybersecurity. By treating system event logs as words in a formal language, we can apply the RPNI algorithm to infer minimal deterministic finite automata from observed traces. We evaluate this approach through a case study on the Cyber Operations Research Gymnasium (CybORG), a widely-used simulation framework for training defensive agents using machine learning. We analyze the structural properties of the inferred automata and assess their empirical fidelity with respect to the semantics of CybORG. Our results show that accurate formal models can be learned from a relatively small number of traces, suggesting a promising path toward more automated and data-driven approaches to cybersecurity.

ABSTRACT. We introduce the tool HyperQB2.0, the first highly efficient push-button bounded model checker (BMC) for hyperproperties. HyperQB takes as input a model in NuSMV or Verilog and a formula expressed in the temporal logics HyperLTL or A-HLTL. The core decision procedures to implement BMC are SMT and QBF solvers, enabling verification of finite- and infinite-state programs. HyperQB offers command-line and standalone graphical, and web-based interfaces. Based on the selection of either bug-hunting or synthesis, instances of counterexamples or path witnesses are returned. The tool is entirely implemented in Rust and we report on successful and effective model checking results for a rich set of experiments on a variety of case studies with rigorous performance comparison and contrast with similar tools.

ABSTRACT. We present a theorem-proving-based technique for verifying deadlock freedom of CSP-style concurrent models in Isabelle/HOL. The approach addresses challenges that are difficult to handle using model checking alone, including infinite state spaces, compositional reasoning in the presence of shared variables, and the need for mechanised proofs. Our main contribution is a coinductive characterisation of deadlock freedom that is equivalent to the standard CSP refinement-based definition, but is more amenable to automated reasoning in an interactive theorem prover. To support reasoning about shared variables, we introduce an assume–guarantee strategy that enforces invariants within transition semantics. The technique is generally applicable to CSP specifications that model shared variables using standard CSP constructs. In particular, we consider the semantics of RoboChart, a domain-specific modelling language for robotic control software, which we mechanise in Isabelle via a shallow embedding in HOL-CSP, and implement automated proof methods. The approach is evaluated on three case studies, including two RoboChart models of industrial robotic systems.

ABSTRACT. Schröer et al. developed a verification infrastructure for rapid prototyping of automated verification techniques for probabilistic programs (PPs), which is based on the quantitative intermediate verification language HeyVL. In a nutshell, users encode programs, specifications, and proof rules into a single HeyVL program. The verification conditions obtained from such a HeyVL program are then discharged with SMT solvers or probabilistic model checkers. However, ensuring that a HeyVL encoding is correct can be subtle and error-prone, just like reasoning about PPs in general. In this paper, we develop mechanized foundations for writing formal correctness proofs for both HeyVL encodings and PP verification techniques that are grounded in the basics of probability theory. To this end, we formalize Markov decision processes (MDPs) - a standard model for assigning operational semantics to PPs. We construct suitable probability spaces for MDPs to ground them in probability theory. Furthermore, we develop least fixed-point characterizations of expected total costs of MDPs, which are useful for relating program logics or denotational semantics to an operational MDP semantics. We apply these characterizations to formalize sound weakest-precondition-style calculi for both partial and total correctness reasoning about the expected behavior of PPs with unbounded loops, nondeterminism, and conditioning. Finally, we develop a deep embedding of the HeyVL intermediate verification language. We apply the above machinery to prove the correctness of various existing HeyVL encodings. During that process, we improved the original HeyVL encoding of an invariant-based proof rule for loops. All of our results have been formalized in the interactive theorem prover Lean on top of mathlib.

ABSTRACT. We present a sound and complete unification procedure for deterministic higher-order patterns, a class of simply-typed lambda terms introduced by Yokoyama et al. which comes with a deterministic matching problem. Our unification procedure can be seen as a special case of full higher-order unification where flex-flex pairs can be solved in a most general way. Moreover, our method generalizes Libal and Miller's recent functions-as-constructors higher-order unification (FCU) by dropping their global restriction on variable arguments, thereby losing the property that every solvable problem has a most general unifier. In fact, minimal complete sets of unifiers of deterministic higher-order patterns may be infinite, so decidability of the unification problem remains an open question.

ABSTRACT. Treating syntactic equality as a logical connective---governed by left- and right-introduction rules within the sequent calculus---offers an elegant and powerful approach to term identity. This treatment of equality allows for the derivation of core mathematical principles, such as Peano’s axioms (excluding induction), and serves as a foundation for the Abella interactive proof assistant. However, integrating this equality into automated proof search remains challenging. We present a proof search procedure that extends unification to handle the complexities of quantifier alternation and equations that occur in both positive and negative occurrences. While established logical frameworks such as lambda Prolog and LF lack direct support for this kind of equality, our procedure enables a lightweight logical framework that addresses this gap. Our system enables unification-aware proof search across a diverse range of first-order sequent calculi that can directly use this form of equality.

ABSTRACT. Building on the small-model constructions for Åqvist’s deontic logics (E, F, F+(CM), and G), we present Deo-SMT, an SMT-based reasoner implemented in Z3 for validity checking and countermodel generation. These logics correspond to well-known conditional systems: F+(CM) extends Preferential Conditional Logic with reflexivity and absoluteness, while G corresponds to Lewis’s VTA. Deo-SMT provides countermodel visualizations as text, matrices, and directed graphs. It outperforms the existing Isabelle/HOL approach and offers a lightweight, user-friendly interface for normative reasoning.

ABSTRACT. We describe grind, an SMT-inspired proof automation tactic for Lean 4. Unlike hammer-style tools that translate proof obligations into external logics and invoke external ATP and SMT solvers, grind works natively in the Calculus of Inductive Constructions, producing kernel-checkable proof terms without any soundness compromises. At its core, grind combines congruence closure for dependent type theory with E-matching and a suite of satellite solvers for linear integer arithmetic, linear arithmetic over ordered modules, polynomial equations over commutative (semi)rings, and associative-commutative operators. Each satellite solver is parameterized by Lean's typeclass mechanism, enabling it to operate over any type implementing the appropriate algebraic interface rather than only hardcoded numeric types. Users can extend grind with new theory solvers through a plugin API, control theorem instantiation through a constraint system on E-matching patterns, and inspect the internal state through an interactive mode with a domain-specific language for navigating the solver. An annotation system with automatic pattern selection enables libraries to declare how their theorems should be used by grind. The tactic ships with Lean and is used extensively in Mathlib, CSLib, and major formalization projects including the Prime Number Theorem formalization and Terence Tao's formalization of Analysis I.

ABSTRACT. Satisfiability Modulo Theories (SMT) solvers are widely used in formal verification.In program analysis, users often encounter queries that differ only by simple syntactic mutations and are logically equivalent. These mutations typically include assertion reordering, symbol renaming, antisymmetric relation inversion, and commutative operand reordering. However, such minor changes can cause runtimes to vary by orders of magnitude. This variability reduces the predictability required for industrial-scale verification and remains a critical challenge. This paper presents SMTStabilizer, a tool that improves the stability of SMT solvers via context-driven normalization. Since complete input normalization has been shown to be as hard as the graph isomorphism problem, SMTStabilizer adopts an approximate normalization strategy to avoid the high cost of exact normalization. The framework converts formulas into a structured representation and propagates structural information across nodes, so that each node becomes aware of its surrounding context. Using these context information, SMTStabilizer derives a consistent ordering over subformulas. This process yields a nearly canonical form that remains consistent across isomorphic inputs. SMTStabilizer also leverages pruning techniques utilizing the syntactic structure of SMT to reduce the normalization time. An evaluation with Z3 and cvc5 on millions of queries shows that SMTStabilizer improves the solvers' stability to over \(98\%\) under 10 random mutations.

ABSTRACT. Reasoning about array data structures is a key requirement for many applications in hardware and software verification, especially in combination with machine integers. The Satisfiability Modulo Theories (SMT) theory of extensional arrays provides array read and write operators and allows extensionality over arrays. This is sufficient to express many aspects of computer aided verification, but lacks succinctness to efficiently deal with arrays that are initialized with a default value. Existing procedures for extending the SMT-LIB theory of arrays with support for constant arrays are limited to arrays with infinite index domains, and existing implementations in SMT solvers only support a fragment of the theory for finite index domains. In this paper, we present a novel decision procedure for the theory of arrays with constant arrays that supports arbitrary index domains and is not limited to the infinite case. We present our procedure as an abstract calculus and show its refutational and satisfiability soundness. We implement a decision procedure based on our calculus in the state-of-the-art SMT solver Bitwuzla and evaluate its performance on a diverse collection of benchmarks and use cases.

ABSTRACT. We generalize an efficient automata-based approach to string constraint solving–the stabilization-based method behind the solver Z3-Noodler–to support relational constraints represented by finite-state transducers (useful, for example, for modelling replaceAll constraints). We focus on an efficient treatment of length constraints by reducing the need for expensive concatenation elimination, which is a major bottleneck in automata-based string solving. We also propose powerful heuristics that significantly improve performance in practice. Implemented on top of Z3-Noodler, our method vastly outperforms existing solvers on benchmarks with relational constraints–it solves more instances and runs orders of magnitude faster.

ABSTRACT. Lagrangian-based duality, traditionally applied in optimization, has recently been generalized to serve as the basis for a unifying framework for primal-dual search algorithms in the context of program verification and automated reasoning. In this paper, we analyze Quantified Satisfiability Modulo Theories (QSMT) algorithms using this framework. Interestingly, our Lagrangian-based analysis reveals that three recently proposed algorithms for quantified linear real arithmetic (LRA) share a common structure, and that their main differences lie in the approach to a certain problem, namely model-based projection for \(\exists\forall\)-formulas. Moreover, in the course of this Lagrangian-based analysis, we identify an issue with the progress property of one of the algorithms, propose a way to fix the issue, and experimentally demonstrate that the proposed fix improves performance.

ABSTRACT. This tool paper presents the latest (2026) version of Mallob – a distributed platform for automated reasoning on demand. Mallob features a world-leading distributed SAT solving engine, which is the first of its kind that supports proof checking, incremental SAT queries, and flexible (re-)scheduling of computational resources. Exploiting this technology, Mallob features further engines relevant for verification, such as MaxSAT and SMT solving. We present these use cases, discuss a wide range of experimental results, and reflect on the system’s impact.

ABSTRACT. Ideal functionalities are used to study increasingly complex protocols within the Universal Composability framework. However, such functionalities are often complex themselves, making it difficult to assess whether they truly fulfill their promises. In this paper, we present four attacks on functionalities from various applications (e-voting, SMPC, anonymous lotteries, and smart metering), demonstrating that they do not capture the intuitively expected properties. We argue that ideal functionalities should not merely be justified secure at a high level but rigorously proven to be so. To this end, we propose a methodology that combines game-based proofs and computer-aided verification: ideal functionalities can in fact be treated as protocols, and one can use traditional game-based proofs to study them, where any game-based security property proven on the functionality does transfer to any protocol that realizes it. We also propose fixed versions of the ideal functionalities we studied, and formally define the security properties they should satisfy through a game. Finally, using Squirrel, a proof assistant for protocol security, we formally prove that the fixed functionalities verify the specified game-based security properties.

ABSTRACT. We present a formally-verified (in Lean 4) framework for translating symbolic cryptographic proofs into the computationally-sound ones. Symbolic cryptography is a well-established field that allows reasoning about cryptographic protocols in an abstract way and is relatively easy to verify using proof assistants. Unfortunately, it often lacks a connection to the computational aspects of real-world cryptography. Computationally-sound cryptography, on the other hand, captures this connection much better, but it is often more complex, less accessible, and much harder to verify formally. Several works in the past have provided a bridge between the two, but, to our knowledge, none of them have been implemented in a proof assistant. We close this gap by formalizing the translation from symbolic to computationally-sound cryptography in Lean 4. Our framework is based on the work of Micciancio (Eurocrypt, 2010) and Li and Micciancio (CSF, 2018), which builds on the idea of using co-induction (instead of induction) for reasoning about an adversary's knowledge in a symbolic setting. Our work encompasses (1) the formalization of the symbolic cryptography framework, (2) the formalization of the computationally sound cryptography framework, and (3) the formalization of the translation between the two. We also provide (4) an extended example of circuit garbling, which is a well-known cryptographic protocol frequently used in secure multi-party computation. We believe that our work will serve as a foundation for future research in the area of formal verification of cryptographic protocols, as it enables reasoning about cryptographic protocols more abstractly while still providing a formally verified connection to the computational aspects of real-world cryptography.

ABSTRACT. Hybrid arguments are prevalent in cryptographic security proofs, however, existing mechanizations in proof assistants are not as general as they could be. In this paper, we prove a general theorem about the admissibility of hybrid arguments that encompasses the query-counting, multi-instance, and nested case. We present three case studies about public-key encryption, which demonstrate the generality of the theorem. The results of this paper are achieved in the setting of state-separating proofs and the theory is integrated into and the case studies are mechanized in Nominal-SSProve.

ABSTRACT. Computer-aided cryptography (CAC) provides strong guarantees through mechanized proofs of security. Squirrel is a proof assistant specialized in CAC, but is restricted to the asymptotic setting, which limits its applicability. Recent theoretical work adapted Squirrel’s underlying logic to the concrete setting through the introduction of a higher-order logic with errors. While this allows to prove precise security bounds on paper, it only provides a low-level logical calculus which lacks an implementation. Thus, it falls short of the CAC aims. In this paper, we use this low-level calculus to build the full-fledged set of features used in a proof assistant such as Squirrel, focusing on reachability reasoning. We design higher-level logical mechanisms on top of this logic, including proof context management, introduction patterns, and bound-annotated tactics. To do so, we need to introduce a proof term calculus with dedicated features for bounds, for which we design an elaborator. This elaborator automatically infer most bound-related manipulations, improving usability and reducing user inputs, and we theoretically argue for its usability through an erasability theorem. All these improvements have been implemented in Squirrel, and we provide empirical evidence of the applicability of our framework through case studies.

ABSTRACT. Formal methods are becoming an important tool for ensuring correctness and security of cryptographic constructions. However, the support for certain advanced proof techniques, namely rewinding, is scarce among existing verification frameworks, which hinders their application to complex schemes such as multi-party signatures and zero-knowledge proofs. We expand the support for rewinding in EasyCrypt by implementing a version of the general forking lemma by Bellare and Neven. We demonstrate its usability by proving EUF-CMA security of Schnorr signatures.

ABSTRACT. In imperative and object-oriented languages, programmers often define relations such as equality or orderings between instances of structs or classes. These object relations must satisfy well-known algebraic properties, such as reflexivity, transitivity, etc. Violations may cause standard library components, such as collections, to behave incorrectly. Crucially, these properties must hold across types, for instance, when comparing instances of different classes. However, studies show that they are commonly violated, and existing techniques for verifying them are non-modular; they give no guarantees if any types are present at runtime that were not known at verification time. Our key idea is to express algebraic properties in a novel, expressive normal form that allows us to statically identify, for each type $T$ and relation $R$, a set of other types that are relevant for the correctness of $R$ in $T$. We prove the intended algebraic properties of $R$ between $T$ and each type in this set. This approach is generic: it applies to different relations (such as equality and orderings), to various imperative and object-oriented languages, and to multiple program logics. We show how it can be used in standard deductive verification tools by encoding the relevant proof obligations using a simple source-to-source rewriting. We implement our technique for the equality relation in the Python verifier Nagini and evaluate it on challenging benchmarks using both Nagini and Dafny, demonstrating its practical applicability and effectiveness.

ABSTRACT. We present ZipLex, a verified framework for invertible linear-time lexical analysis following the longest match semantics. Unlike past verified lexers that focus only on satisfying the semantics of regular expressions and the longest match property, ZipLex also guarantees that lexing and printing are mutual inverses. Thanks to verified memoization, it also ensures that the lexical analysis of a string is linear in the size of the string. Our design and implementation rely on two sets of ideas: (1) a new abstraction of token sequences that captures the separability of tokens in a sequence while supporting their efficient manipulation, and (2) a combination of verified data structures and optimizations, including Huet’s zippers and memoization with a verified imperative hash table. We implemented and verified ZipLex using the Stainless deductive ver- ifier for Scala. Our evaluation demonstrates that ZipLex supports real- istic applications such as JSON processing and lexers of programming languages, and behaves linearly even in cases that make flex-style ap- proaches quadratic. ZipLex is two orders of magnitude faster than Ver- batim++, showing that verified invertibility and linear-time algorithms can be developed without prohibitive cost. Compared to Coqlex, ZipLex also offers linear (instead of quadratic) time lexing, and is the first lexer that to come with invertibility proofs for printing token sequences.

ABSTRACT. Efforts to verify Zero-Knowledge Proof circuit encodings have highlighted the challenge of verifying operations proving the correctness of quantifier-free statements that make use of both bitvector and finite field operations. Existing verification workflows are either manual or rely on SMT solvers, which scale poorly on some classes of problems for reasons that include difficulties with conversion operators and challenges reasoning about inequalities. To address these limitations, we present a novel Lean tactic BitModEq that leverages range lemmas and case analysis to produce verified translations from finite fields to bitvectors. Our approach, combined with bit-blasting, outperforms state-of-the-art SMT solvers, solving 19% more ZKP arithmetization benchmarks.

ABSTRACT. We present the Cooperating Proof Calculus (CPC), an evolving set of proof rules encompassing all inferences used in the mainstream features of the SMT solver cvc5. CPC consists of 585 proof rules, which weformalized in roughly 6400 lines of definitions in the logical framework Eunoia. Eunoia proofs are independently checkable by the proof checker Ethos. This paper gives a detailed summary of CPC, surveying its proof rules over its major components. Having instrumented cvc5 to generate CPC proofs in Eunoia, we show that the solver is capable of generating fine-grained CPC proofs, with no proof holes, for all benchmarks in the SMT library except those in logics with floating points, which are currently not supported. This results in roughly 913 million proof steps using 427 unique proof rules. We also discuss ongoing work in the proof assistants Lean and Isabelle to verify the correctness of CPC.

ABSTRACT. Burrow is a proof framework for weak memory mapping proofs. Those mappings appear as optimizations and translations between languages inside compilers and binary translators. However, their mechanized proofs, when defined over formal axiomatic weak memory semantics, are often large and complex. In this paper, we discuss the proof primitives provided by Burrow which simplify mechanizing those mapping proofs and help to prove many lemmas generally. To demonstrate the benefits of these primitives, we use Burrow to prove a conjectured mapping from x86 to Arm correct.

ABSTRACT. We present Velvet—a Dafny-style verifier for imperative programs embedded in the Lean proof assistant. Like Dafny, Velvet supports reasoning about effectful programs featuring mutable state, loops, and non-determinism. Unlike Dafny, Velvet seamlessly combines automated SMT-based proofs with the interactive proof mode of the Lean proof assistant, in which it is embedded, thus enabling multi-modal proofs. Implemented as a Lean library, Velvet enjoys interaction with the rest of the Lean ecosystem, and in particular, with its automation tactics and rich library of mathematical theories. In this paper, we give a tour of Velvet’s features, outline the techniques underlying its implementation, and evaluate its performance and expressivity in comparison with Dafny.

ABSTRACT. Separation logic proofs of heap-manipulating programs require careful accounting of objects and pointers in memory. On paper, these proofs are often accompanied by heap memory diagrams that help authors and readers visualize and track the evolution of the program's abstract state. However, users of interactive theorem provers must instead work with plain-text notations that obscure object relationships. This paper presents the first automatic visualization and animation library for separation logic heap predicates. Four key features make the library practical. First, it supports animating across proof steps. Second, it offers a DSL to specify how custom user-specified predicates should be visualized. Third, it is straightforward to port to new separation logic frameworks. And fourth, it can be used in browsers and IDEs, during and after proof development. We demonstrate these features by implementing frontends for CFML and Iris, integrating with Alectryon and VsRocq, and reproducing hand-drawn diagrams found in published materials.

ABSTRACT. Neural approaches to theorem proving require robust infrastructure for interfacing with interactive theorem provers (ITPs), extracting structured proof data, and executing proof search at scale. However, existing tooling is often assistant-specific and oriented toward interactive, file-level execution, making repository-scale analysis and parallel experimentation challenging. We present ProofWala, a multilingual proof engineering framework built around itp-interface, a reusable library for programmatic interaction with ITPs. For Lean 4, we implement a meta-programmed interaction layer that executes inside the elaborator, enabling semantically faithful tactic-level tracing together with declaration- and dependency-level extraction across entire repositories. This design extends beyond traditional REPL-style interaction by supporting project-wide analysis, environment cloning, and pooled execution of proof states. The implementation is robust across Lean 4 versions after 4.15.0 with forward compatibility support. The same interface abstraction supports tactic execution and data extraction for multiple versions of Rocq, yielding a unified cross-assistant pipeline.Built on this infrastructure, ProofWala provides standardized multilingual proof datasets, model training utilities, and parallel proof search algorithms. Using the framework, we demonstrate that multilingual training across Lean and Rocq enables cross-lingual and cross-domain transfer, with mixed-training models outperforming assistant-specific baselines on the standard prove-at-k metric. We open-source the full framework, including the parallel proof search module, the itp-interface library, multilingual datasets, and trained models, providing a scalable foundation for proof mining, neural theorem proving, and cross-assistant experimentation.

ABSTRACT. Termination---proving there are no inputs on which a function runs forever---is one of the most fundamental problems in software verification, and competitions comparing termination analysis tools have run for over twenty years. We integrate two state-of-the-art, open-weight LLMs with a theorem prover’s built-in automation to generate termination proofs, solving 39\% more problems than the best LLM alone and more than tripling the number solved by the built-in analysis on our benchmark. This is the first, to our knowledge, integration of an LLM with a termination-analysis algorithm, and is generalizable to any theorem prover based on a functional language. Our design is informed by nine ablations considering what theorem-prover feedback helps the LLM and four experiments on how the model decomposes problems.

ABSTRACT. Large-scale formalization projects in Lean rely on blueprints: structured dependency graphs linking informal mathematical exposition to formal declarations. While blueprints are central to human collaboration, existing tooling treats the informal (LaTeX) and formal (Lean) components as largely decoupled artifacts, leading to maintenance overhead and limiting integration with AI automation. We present LeanArchitect, a Lean package for extracting, managing, and exporting blueprint data directly from Lean code. LeanArchitect introduces a declarative annotation mechanism that associates formal declarations with blueprint metadata, automatically infers dependency information, and generates LaTeX blueprint content synchronized with the Lean development. This design eliminates duplication between formal and informal representations and eases fine-grained progress tracking for both human contributors and AI-based theorem provers. We demonstrate the practicality of LeanArchitect through the automated conversion of several large existing blueprint-driven projects, and through a human--AI collaboration case study formalizing a multivariate Taylor theorem. Our results show that LeanArchitect improves maintainability, exposes latent inconsistencies in existing blueprints, and provides an effective interface for integrating AI tools into real-world formalization workflows.

ABSTRACT. We present a formalized theory of context-free grammars and their links to finite automata. In particular we focus on first-time formalizations of an executable translation into Greibach Normal Form, the Chomsky-Schützenberger Representation Theorem and Parikh's Theorem.

ABSTRACT. A string diagram is a two-dimensional graphical representation that can be described as a one-dimensional term generated from a set of primitives using sequential and parallel compositions. Since different syntactic terms may represent the same diagram, this syntax is quotiented by a collection of coherence equations expressing equivalence up to deformation. This work lays foundations for automated reasoning about diagrammatic equivalence, motivated primarily by the verification of quantum circuit equivalences. We consider two classes of diagrams, for which we introduce normalizing term rewriting systems that equate diagrammatically equivalent terms. In both cases, we prove termination and confluence with the help of the proof assistant Isabelle/HOL.

ABSTRACT. Pitts' proof-theoretic technique for uniform interpolation, which generates uniform interpolants from terminating sequent calculi, has only been applied to logics on an intuitionistic basis through single-succedent sequent calculi. We adapt the technique to the intuitionistic multi-succedent setting by focusing on the intuitionistic modal logic KM. To do this, we design a novel multi-succedent sequent calculus for this logic which terminates, eliminates cut, and provides a decidability argument for KM. Then, we adapt Pitts' technique to our calculus to construct uniform interpolants for KM, while highlighting the hurdles we overcame. Finally, by (re)proving the algebraisability of KM, we deduce the coherence of the class of KM-algebras. All our results are fully mechanised in the Rocq proof assistant, ensuring correctness and enabling effective computation of interpolants.

ABSTRACT. In this paper, we present the first proof-of-concept framework for end-to-end formally verified graph generation. Our approach integrates SAT modulo symmetries with the Lean proof assistant, providing a unified, machine-checked verification pipeline that spans high-level graph-theoretic specifications, propositional encodings, symmetry-breaking mechanisms, and solver-based search. By formalizing graph invariance and symmetry reasoning within Lean, we eliminate common trust assumptions and obtain fully certified non-existence results. We evaluate the framework on three benchmark classes of graph-generation problems, showing practical feasibility on nontrivial unsatisfiable instances.

ABSTRACT. Both higher-order logic and dependent types are popular features for languages used for the formalization of complex domains. Recently DHOL was introduced as a language that provides the expressivity of dependent types while retaining the general feel of higher-order logic. Since then multiple extensions and theorem provers have been developed, and DHOL was adopted as the first TPTP standard for using dependent types in automated theorem provers. However, the literature lacks a model theoretical semantics for DHOL. The present paper fills in this gap. It introduces both standard models and Henkin models and proves soundness and completeness. Considerable care went into keeping the formulation as close to the usual definitions for FOL and HOL and thus most intuitive. However, we had to make a significant generalization to Henkin models for HOL in order to obtain completeness in the presence of dependent types. Our results will allow for extending semantic methods for HOL to DHOL and can serve as a model-theoretical reference point for showing the equivalence of theorem provers.

ABSTRACT. This paper presents a certified theorem prover for Grzegorczyk logic (Grz) implemented in the general-purpose proof assistant HOL Light. Our prover builds on original HOL Light formalisations of modal adequacy for Grz with respect to finite partially ordered frames, and on the standard full and faithful translation of Grz into Gödel–Löb logic (GL). This formalised embedding allows us to extend the range of modal systems supported by the HOLMS library for automated modal reasoning, and constitutes a new methodology experimented in our framework, being the first logic added to the library through a modal translation. The deductive engine performs an automated proof search in the labelled sequent calculus for GL. When the proof search on the translated formula succeeds, the system returns a HOL Light theorem certifying provability of the original Grz formula. When proof search terminates negatively, the system constructs a verified GL countermodel and thus certifies that the original formula is not provable in Grz.

ABSTRACT. A DFA separates two disjoint languages $L_1$ and $L_2$ if it accepts every word in $L_1$ and rejects every word in $L_2$. Algorithms for active learning of small separating DFAs have many applications, e.g.\ for learning network invariants, learning contextual assumptions in compositional verification, learning state machines from large amounts of log data, and learning bug pattern descriptions. In this paper, we propose a new learning algorithm, inspired by $L^{\#}$, that learns a minimal separating DFA for disjoint languages $L_1$ and $L_2$ if one exists. Experimental results show that our algorithm significantly outperforms existing active learning algorithms on both randomly generated and industrial benchmarks.

ABSTRACT. Emerson-Lei automata, which allow arbitrary Boolean combinations of $\mathtt{Fin}$ and $\mathtt{Inf}$ acceptance conditions, provide a unifying framework for $\omega$-automata but pose significant challenges for determinization. The previous best algorithm relies on a \texttt{removeFin} transformation that introduces an exponential blow-up in the state space before determinization even begins. We present a new determinization algorithm that completely bypasses this bottleneck. Our key insight is that each disjunct of an Emerson-Lei condition in DNF corresponds directly to a \emph{one-Fin automaton}---a restricted form of Streett automaton whose structure enables more efficient determinization via H-Safra trees. By exploiting this connection, we establish an upper bound of \[ 2^{O\!\big(3^{|\alpha|/3} \cdot (n \log n + n|\alpha| \log |\alpha|)\big)} \] where $n$ is the number of states and $|\alpha|$ is the acceptance condition size. This improves the exponent over the previous best bound by a factor of $2^{2|\alpha|}/3^{|\alpha|/3}$, an exponential improvement in the acceptance condition complexity.

ABSTRACT. We present an SMT-based active learning algorithm for non-deterministic weighted automata (WFAs) as a practical and robust alternative to Hankel/L*-style methods. Our algorithm is parametric in a given semiring and, if it terminates, guaranteed to produce minimal WFAs. We prove partial correctness and provide a sufficient termination condition, which in particular implies termination for all finite semirings. Our extensive experimental evaluation shows that our algorithm is capable of learning numerous minimal WFAs over both finite and infinite semirings, vastly outperforms a naive baseline, and is competitive with a state-of-the-art algorithm while producing significantly smaller automata and requiring less interaction with the teacher.

ABSTRACT. In many verification tasks, system models do not correspond to the focused and idealized models that appear in research literature. In practice, models usually contain components and execution paths that are irrelevant to the property being verified or have only a minor effect on it. Compositional verification presents a practical method for coping with the larger and less targeted models found in such settings. In this paper, we present an automated compositional framework for verifying timed safety properties in networks of timed automata. We show as a main result that the weakest environment assumption, commonly used in compositional reasoning, may in general fail to be recognizable within the timed automata formalism. This negative result motivates shifting the focus to the complement language of violation-inducing timed words, for which we establish recognizability using timed automata with silent transitions. We provide an algorithm for its construction and reduce its size by retaining only the parts directly relevant to the property. The synthesized assumption is later applied to verify the original system. This provides a sound and complete basis for compositional verification of timed automata, including the novel ability to handle automata with multiple clocks and non-deterministic behavior. Our results broaden the applicability of assume–guarantee verification techniques in timed automata and show substantial reductions in the size of the state-space, outperforming monolithic methods on a range of case studies.

ABSTRACT. Workflow nets are a variant of Petri nets used for modelling business processes. Central decision problems are soundness problems; one popular variant is called generalised soundness. These problems intuitively ask whether initiated processes can be finalised. We introduce weighted soundness, which strengthens the classical concepts of soundness. In weighted soundness, we bound the weight (typically length) of runs to finalise processes. This allows one to require processes to be finalised within a restricted budget. We provide multiple reasons supporting the relevance of weighted soundness. Our theoretical analysis shows that weighted soundness is provably simpler than classical soundness. Our main result is that weighted generalised soundness is co-NP^NP-complete, while (unweighted) generalised soundness is known to be PSPACE-complete. Our practical analysis shows that on standard benchmarks classical soundness coincides with weighted soundness, if the weight is set to the number of transitions in the workflow net. Furthermore we analyse the Inductive Miner algorithm, one of the most popular algorithms generating workflow nets from event logs. Inductive Miner is known to guarantee the output workflow nets to be generalised sound. We show that it outputs workflow nets that are weighted generalised sound with a weight linear in the size of the event alphabet. Finally, we generalise reduction techniques from soundness to weighted soundness. Such reductions are crucial in implementations of soundness algorithms.

ABSTRACT. Partially Observable Markov Decision Processes (POMDPs) are the standard framework for decision-making under uncertainty. While sampling-based methods scale well, they lack formal correctness guarantees, making them unsuitable for safety-critical applications. Conversely, formal synthesis techniques provide correctness-by-construction but often struggle with scalability, as general POMDP synthesis is undecidable. To bridge this gap, we propose a synthesis framework that integrates sampling, automata learning, and model-checking. Inspired by Angluin’s L* algorithm, our approach utilizes sampling as a membership oracle and model-checking as an equivalence oracle. This enables the synthesis of finite-state controllers with formal guarantees, provided the sampling-induced policy is regular. We establish a relative completeness result for this framework. Experimental results from our prototypical implementation demonstrate that this method successfully solves threshold-safety problems that remain challenging for existing formal synthesis tools. We believe our algorithm serves as a valuable component in a portfolio approach to tackling the inherent difficulty of POMDP synthesis problems.

ABSTRACT. We present TACO, a toolsuite for the development and automatic verification of fault-tolerant and threshold-based distributed algorithms. Our toolsuite implements three approaches for model checking threshold automata in different decidable fragments known from the literature and two semi-decision procedures going beyond these decidable fragments. Moreover, TACO is a modular, extensible, and well-documented framework for developing algorithms and tools for threshold automata. We present important features, give an overview of the implemented algorithms, and evaluate their performance experimentally.

ABSTRACT. Quantitative automata (QAs) extend finite-state $\omega$-automata with weighted transitions to specify quantitative system properties. However, their finite weight sets rule out properties like average response time, where response times can be arbitrarily large. Nested quantitative automata (NQAs) overcome this limitation: a parent automaton spawns child automata to compute unbounded values over finite subwords and aggregates them into a final result. Despite this expressiveness, NQAs have lacked practical tool support to date. We address this gap by extending the Quantitative Automata Kit (QuAK), a software tool for QA analysis, to support NQAs. Our core contribution is implementing a suite of flattening procedures that reduce NQAs to QAs, leveraging QuAK's existing decision procedures. The tool handles all decidable combinations of parent aggregators (including limits and averages) and child functions (extrema and monotonic or bounded summations). Experiments on response-time and resource-consumption benchmarks demonstrate QuAK's effectiveness.

ABSTRACT. In recent years, numerous techniques were developed to automatically prove termination of different kinds of probabilistic programs. However, there are only few automated methods to disprove their termination. In this paper, we present the first techniques to automatically disprove (positive) almost-sure termination of probabilistic term rewrite systems. Disproving termination of non-probabilistic systems requires finding a finite representation of an infinite computation, e.g., a loop of the rewrite system. We extend such qualitative techniques to probabilistic term rewriting, where a quantitative analysis is required. In addition to the existence of a loop, we have to count the number of such loops in order to embed suitable random walks into a computation, thereby disproving termination. To evaluate their power, we implemented all our techniques in the tool AProVE.

ABSTRACT. We investigate the uniform fluted fragment, a subfragment of the fluted fragment obtained by imposing the uniformity restriction on Boolean combinations. First, with a novel trick in model construction, we prove that the uniform fluted fragment has an exponentially bounded model property. It follows that, unlike the full fluted fragment (where satisfiability is non-elementary), satisfiability in this subfragment is NExpTime-complete. Second, we formulate a bisimulation for the subfragment, and establish a characterization of its expressive power in the style of van Benthem. Finally, we show that the uniform fluted fragment is equi-expressive with the uniform forward fragment (if we consider only sentences), and that satisfiability in the latter is also NExpTime-complete.

ABSTRACT. Kleene algebras are an algebraic abstraction of regular expressions, one of the central notions in computer science. While the equational theory of Kleene algebras is known to be decidable, reasoning from finite sets of hypotheses (Horn theory) quickly becomes undecidable. This happens even for simple classes of hypotheses which themselves do not involve Kleene star. One of such classes of hypotheses is formed by sum-of-letters hypotheses, of the form $a \leq b_1 + \ldots + b_k$, where $a, b_1, \ldots, b_k$ are letters. In the present paper, we strengthen the undecidability result proved for this class of hypotheses by Doumane et al. (2019) and establish the exact complexity --- $\Sigma^0_1$-completeness. Moreover, we strengthen our result and show the same complexity bounds for one fixed set of sum-of-letters hypotheses. We also accompany this result with a decidability one, for comparison.

ABSTRACT. Automatically identifying temporal properties from observations of a system's behavior provides valuable insight into that system's inner workings. Temporal properties are often expressed in temporal logics, such as Computation Tree Logic (CTL). Existing approaches to learning CTL specifications from observations rely on constraint-solving by encoding the search for formulas into a satisfiability problem that perfectly separates observations that the system can (positive) or cannot (negative) perform. While adequate in noise‑free settings, these methods often struggle with noisy data, such as incomplete executions or mislabeled traces, and scale poorly to large inputs. To overcome these limitations, we propose a neural approach for learning CTL specifications from positive- and negative-labeled observations represented as transition systems. Our method employs a neural network in which neurons encode the presence of CTL operators at specific positions. After training, a deterministic extraction procedure converts network weights into interpretable CTL formulas. In contrast to satisfiability‑based learning approaches, our framework efficiently produces high‑quality specifications even under noisy data conditions. It supports arbitrary CTL formulas up to a user-defined size budget and consistently yields accurate results within short computation times, demonstrating that neural architectures can provide a fast and noise-tolerant method for inferring temporal properties.

ABSTRACT. Natural-language proof assistants such as Naproche and our own system Natty can translate a mathematical text in controlled natural language into a series of logical formulas to be verified. Natty also contains an automatic prover that is designed to quickly verify formulas representing proof steps. Natty's prover is based on superposition, but uses a variety of techniques that are unusual for superposition-based provers, including commutative unification and a form of rewriting that sometimes preserves the rewritten clause. To evaluate this prover and others, we have produced a test suite called TextbookMath containing over 150 theorems and their proofs, which we transcribed from a classic number systems textbook by Mendelson into N, the controlled natural language of Natty. Natty can read this text and generate a set of over 900 conjectures of higher-order logic, each corresponding to a single proof step in the original Mendelson text. We find that established high-order provers such as E and Vampire can prove only about 85\% of these conjectures using a single strategy with a 5-second timeout. Surprisingly, some of the conjectures they fail to prove look relatively easy and should be provable with only a few superposition steps. Natty's automatic prover can prove about 91\% of these conjectures under a similar time restriction. If we expand the Mendelson text with various intermediate proof steps and lemmas, Natty can completely verify a textbook development of the natural numbers, integers and rationals including 5 of Wiedijk's well-known list of 100 theorems.

ABSTRACT. We present an implemented reasoner for fuzzy order-sorted feature (OSF) logic, supporting fuzzy unification and normalization of OSF terms modulo a sort theory. Fuzzy OSF logic is a knowledge representation and reasoning language based on feature symbols, denoting functions, and sort symbols, denoting fuzzy sets. Sort symbols are organized in a fuzzy subsumption relation that extends to OSF terms, record-like structures representing classes of entities. The unification algorithm for these structures provides a calculus of fuzzy type subsumption. We demonstrate the system's behavior on representative examples, such as computing the membership degree of an instance to a sort, and computing subsumption degrees between sorts and OSF terms. We also report a comparison with a resolution-based fuzzy logic programming system.

ABSTRACT. We present a formalization of combinatorial design theory in Lean 4, with a focus on balanced incomplete block designs (BIBDs) and their algebraic properties. The flagship result is the Bruck-Ryser-Chowla theorem, which gives the best known necessary conditions for the existence of a symmetric BIBD, formalized here in a proof assistant for the first time. Reaching this result required us to develop substantial infrastructure beyond combinatorics: we formalize Witt's cancellation theorem for quadratic forms, prove new results on matrix congruence and block matrices, and extend Mathlib's linear algebra library in several directions. We also provide the first formalization of Fisher's inequality in Lean and the first formalization of the Kramer-Mesner theorem in any proof assistant, along with a reusable double-counting argument that supports standard combinatorial reasoning. The cross-domain nature of these contributions reflects a distinctive feature of design theory itself: it draws on and feeds back into many areas of mathematics, making it a particularly rewarding target for formalization within a large-scale library like Mathlib.

ABSTRACT. We present a Lean 4 formalization of the de Finetti–Ryll-Nardzewski theorem for infinite sequences of random variables on standard Borel spaces, establishing that every exchangeable sequence is conditionally i.i.d. The development closely follows Kallenberg's modern treatment of probabilistic symmetries and formalizes three distinct proofs of the key implication, with the second and third formalized for real-valued square-integrable sequences: (i) a reverse‑martingale argument due to Aldous, (ii) an elementary L² approach based on contractability bounds and Cesàro convergence, and (iii) an ergodic‑theoretic proof via the Koopman operator and the mean ergodic theorem. The library contains over 42,000 lines of code and was completed in three months with extensive use of Claude and GPT models, together with a reusable Lean proof-engineering skill for agentic coding systems developed during the project. The three proofs share a uniform common ending, so each route had to produce the same finite conditional-factorization interface before the final conclusion. This provided a cross-check on these independent routes during AI-assisted development.

ABSTRACT. We present an ongoing effort to build a framework and a library in Isabelle/HOL for formalising primal-dual arguments for the analysis of algorithms. We discuss a number of example formalisations from the theory of matching algorithms, covering classical algorithms like the Hungarian Method, widely considered the first primal-dual algorithm, and modern algorithms like the Adwords algorithm, which models the assignment of search queries to advertisers in the context of search engines.

ABSTRACT. This is a brief description of a project that has already autoformalized a large portion of the general topology from the Munkres textbook (which has in total 241 pages in 7 chapters and 39 sections). The project has been running since November 21, 2025 and has as of January 4, 2026, produced 160k lines of formalized topology. Most of it (about 130k lines) have been done in two weeks, from December 22 to January 4, for an LLM subscription cost of about $100. This includes a 3k-line proof of Urysohn’s lemma, a 2k-line proof of Urysohn’s Metrization theorem, over 10k-line proof of the Tietze extension theorem, and many more (in total over 1.5k lemmas/theorems). The approach is quite simple and cheap: build a long-running feedback loop between an LLM and a reasonably fast proof checker equipped with a core foundational library. The LLM is now instantiated as ChatGPT (mostly 5.2) or Claude Sonnet (4.5) run through the respective Codex or Claude Code command line interfaces. The proof checker is Chad Brown’s higher-order set theory system Megalodon, and the core library is Brown’s formalization of basic set theory and surreal numbers (including reals, etc). The rest is some prompt engineering and technical choices which we describe here. Based on the fast progress, low cost, virtually unknown ITP/library, and the simple setup available to everyone, we believe that (auto)formalization may become quite easy and ubiquitous in 2026, regardless of which proof assistant is used.

ABSTRACT. We propose a variant of classic information flow analysis that permits transmission of secrets over a public network, provided that secrets are suitably encrypted. In the style of Dolev and Yao, the intruder controls the network, observing all messages sent, but can only decrypt messages for which they know the decryption key, i.e., those keys which correspond to the security level of the intruder. In contrast to similar previous works we allow the intruder to send arbitrary bit strings as input to the program without any assumption that these inputs are in some sense well-typed. This means that cryptographic messages can enter program variables that were not meant to hold cryptographic messages and become part of computations and conditions. Despite this strong intruder model, we show that a program that satisfies our information-flow analysis also enjoys Dolev-Yao noninterference, a variant of standard noninterference where the intruder cannot break cryptography. The underlying model, which combines operating on actual bit strings with a symbolic intruder model, and the entire result are formalized and proved in Isabelle/HOL.

ABSTRACT. Gradual typing effectively combines the advantages of dynamic and static typing and is utilized in Information Flow Control. The gradual guarantee ensures that removing type annotations does not affect runtime behavior. However, Toro et al. identify a tension between the gradual guarantee and noninterference, leading many gradual security-typed languages to reconcile these two properties. Recently, Chen and Siek’s language λIFC achieves both properties. Nevertheless, their cast calculus suffers from scalability issues and lacks binary operators, which limits its practical use. In this paper, we present a partial cast calculus λp for gradual information security based on the concept of partial label. Partial labels serve as concise representations for security coercions and runtime labels, which simplify the definition of operators related to security labels and facilitate cast reductions within the semantics of λp. Consequently, this calculus effectively support binary operators and can be readily extended to accommodate more complex sets of security labels. We prove both noninterference and the gradual guarantee for λp. Furthermore, we explore extensions concerning the accommodation of unknown references and a semantic interpretation of our partial labels.

ABSTRACT. We present CryptoChoreo, a choreography language for the specification of cryptographic protocols. Choreographies can be regarded as an extension of Alice-and-Bob notation, providing an intuitive high-level view of the protocol as a whole (rather than specifying each protocol role in isolation). The extensions over standard Alice-and-Bob notation that we consider are non-deterministic choice, conditional branching, and mutable long-term memory. We define the semantics of CryptoChoreo by translation to a process calculus. This semantics entails an understanding of the protocol: it determines how agents parse and check incoming messages and how they construct outgoing messages, in the presence of an arbitrary algebraic theory and non-deterministic choices made by other agents. While this semantics entails algebraic problems that are in general undecidable, we give an implementation for a representative theory. We connect this translation to ProVerif and show on a number of case studies that the approach is practically feasible.