arXiv subjects

Joseph Tassarotti

Publications and source records attributed to Joseph Tassarotti.

At least 19 recordsLinked to original sources

arXiv2026

Elton: Urn Resources for Reasoning about Adversarial Probabilistic Programs

Probabilistic programs are important for many applications. For security applications in particular, one is interested in establishing properties that hold in the presence of arbitrary adversaries, i.e., unknown pieces of code. We present Elton, a higher-order separation logic for reasoning about higher-order probabilistic programs utilizing unknown adversarial code. Elton incorporates novel logical facilities for specifying invariants over distributional properties using delayed samplings at the language level, and a new kind of separation-logic predicate called urn resources at the logic level. We show that these extensions are sound and can be erased back to a standard call-by-value semantics. Combined with other features, e.g. invariants and ghost resources, Elton is expressive enough to prove error bounds on a wide range of security examples, some of which are beyond the scope of previous techniques. All proofs are mechanized with the Rocq proof assistant and the Iris separation logic framework.

cs.LO↗

arXiv2026

Verifying Probabilistic Programs in Rust

Recent work has developed many techniques for formally verifying probabilistic programs. However, existing verification frameworks for probabilistic programs are restricted to idealized languages designed for verification. As a result, they cannot be used to verify off-the-shelf probabilistic programs written in standard languages. In contrast, for non-probabilistic programs, a number of verification tools now support verifying realistic code written in widely used languages such as Go, C, and Rust. To verify probabilistic programs written in these languages, it would be useful to be able to reuse, as much as possible, the extensive development work that has gone into such tools. This paper presents Alerus, a framework for verifying probabilistic Rust programs. Alerus is based on Verus, a verification tool for Rust that supports SMT-based automation and separation-logic-inspired reasoning features. Alerus extends Verus with support for probabilistic reasoning while retaining these expressive features. To do so, Alerus uses a lightweight encoding of probabilistic error credits, a form of ghost state for randomized reasoning introduced in the Eris program logic. By deriving an appropriate specification using error credits, Alerus supports verifying the correctness of randomized sampling algorithms. We use this technique to verify several sampling routines for discrete distributions, including samplers for the discrete Gaussian distributions, the alias method, and the fast loaded dice roller. We establish the soundness of our error credit extension by adapting VerusBelt, a recently developed logical relations model of Verus that encodes its features in terms of the Iris separation logic. To do so, we replace the use of Iris's standard weakest precondition in this model with Eris's probabilistic weakest precondition instead. The resulting soundness proof is fully mechanized in Rocq.

cs.PL↗

arXiv2026

Building Extensible Program Logics through Effect Handlers

One strategy for reasoning about programs that have certain kinds of effects is to use program logics that provide specialized rules for reasoning about these effects. However, developing program logics requires skills that are distinct from those needed for using program logics, making the development of new logics challenging and less accessible. Moreover, when developing new logics, it can be difficult to reuse components from prior logics or combine support for different effects. In this paper, we propose an approach for operationally building extensible program logics based on effect handlers. Our starting point is an expressive program logic for reasoning about programs written in a pure, sequential language with support for effect handlers. Within this language, we implement handlers that model concurrency, distributed execution, and crash-recovery behavior. Then, by proving properties about these handlers, we extend the program logic and derive expressive rules for reasoning about these effects. In some cases, this approach leads to stronger reasoning rules than those found in prior program logics targeting these features. In addition, we develop a relational logic for proving contextual refinements between programs using effects. As with unary reasoning, handlers enable this relational logic to be developed in an extensible way.

cs.LO↗

arXiv2026

Completeness of Logical Atomicity for Linearizability in Concurrent Separation Logic

Linearizability is a standard correctness condition for concurrent data structures. It guarantees that operations behave as if they took effect at some atomic instant between their call and return points. Despite the central role linearizability plays, prior work has argued for instead using a style of specification that internalizes the atomicity of operations in terms of the logic's reasoning rules, known as logical atomicity. These logically atomic specifications are intended to be easier to compose inside of the logic than linearizability. Prior work has shown that in the Iris separation logic framework, a certain form of logically atomic specifications implies that a data structure is linearizable. However, the converse remained an open question: for every linearizable data structure, is it always possible to derive a corresponding logically atomic specification? This paper resolves this question in the affirmative. We prove a completeness theorem for Iris that derives a logically atomic specification for any linearizable data structure. As a consequence, we are able to embed a variety of linearizability proof techniques into Iris and use them to derive logically atomic specifications. We apply this to three linearizability proof methods: aspect-oriented linearizability proofs, forward simulations with commit points, and meta-configuration tracking. Using these embeddings, we derive logically atomic specifications for the Herlihy-Wing queue and the Baskets Queue. We furthermore establish a connection between logical atomicity and an encoding of refinement in Iris that has been used in prior logical relations models. This result allows us to transport logically atomic specifications across refinements, which we apply to the Folly MPMC queue implementation. All of the results in this paper have been mechanized in the Rocq Prover.

cs.LO↗

arXiv2026

Mizzle: A Complete Concurrent Incorrectness Logic for Preventing False Alarms in Agentic Bug Finding

Large language models are increasingly used to find bugs in real-world programs, but they also produce a flood of false alarms that waste developers' time. We propose a method to prevent these false alarms by requiring an LLM to accompany each bug report with a machine-checked proof, in a program logic, that the reported bug is real. We follow the approach of incorrectness logics, whose under-approximate reasoning establishes that a claimed behavior is genuinely reachable, and hence a true positive. In our case, however, the logic must model a realistic programming language, have a mechanization so that proofs can be checked, and be complete, so that no real bug is ruled out for want of a derivation. We present Mizzle, an incorrectness separation logic for concurrent programs written in a substantial subset of OCaml, parametric in the notion of incorrectness. We mechanize Mizzle in the Rocq proof assistant on top of the Iris framework, and we prove that it is both sound (that is, it never justifies a false alarm) and complete (that is, every incorrect execution admits a derivation). We instantiate Mizzle with three notions of incorrectness: stuckness (triggering undefined behavior), the non-linearizability of a data structure, and the presence of a race. As a proof of concept, we illustrate how an LLM can use Mizzle in order to certify the existence of a bug.

cs.PL↗

arXiv2026

A Separation Logic for Parallel Time Complexity with Work and Span Credits

We present Parcas, a concurrent separation logic for verifying the parallel time complexity of fork-join programs. In order to abstract from the specifics of the machine, time complexity for parallel programs is given in terms of two metrics: the work, measuring the total number of operations, and the span, measuring the longest chain of sequential dependencies. Together, these two metrics determine the running time on any number of processors. For proving bounds on the work and span, Parcas is equipped with work credits and span credits, logical devices that represent permissions to incur costs. Work credits are a straightforward adaptation of time credits, a standard tool for bounding time complexity of sequential programs, and can be split additively between parallel tasks. Span credits, however, require a fundamentally different treatment. Indeed, the span of the parallel composition of two tasks is the maximum of the span of the two tasks. To account for this, we propose a rule for duplicating span credits at fork points, with each copy tagged by a logical task identifier that restricts which task may spend them. A transfer rule allows unused span credits to be forwarded across sequential compositions to subsequent tasks. The logic is expressive enough to give modular, higher-order specifications for common parallel primitives such as a parallel for loop and a tabulate function. We demonstrate Parcas on several case studies, including parallel prefix sums, parallel merge sort, and a variant of Treiber's lock-free stack that mixes concurrency with parallelism. All the presented results are mechanized in the Rocq prover using the Iris separation logic framework.

cs.PL↗

arXiv2026

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic

Most implementations of sampling algorithms for continuous distributions use floating-point numbers, which introduce round-off errors and approximations. These errors can be difficult to analyze, and can cause security issues when used in algorithms for differential privacy. An alternative is to use exact sampling algorithms based on computable reals, which can lazily generate the digits of a continuous sample to arbitrary precision. However, these algorithms are intricate, and implementing and using them involves a combination of semantically challenging language features, such as probabilistic choice, higher-order functions, and dynamically-allocated mutable state. In this paper we present Continuous-Eris, a higher-order separation logic for verifying the correctness of exact sampling algorithms for computable distributions. To demonstrate Continuous-Eris, we verify the correctness of computable samplers for the uniform, Gaussian, and Laplace distributions, as well as a library for exact real arithmetic for working with generated samples. All of the results in this paper have been verified in the Rocq proof assistant.

cs.LO↗

arXiv2026

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)

We present Foxtrot, the first higher-order separation logic for proving contextual refinement of higher-order concurrent probabilistic programs with higher-order local state. From a high level, Foxtrot inherits various concurrency reasoning principles from standard concurrent separation logic, e.g. invariants and ghost resources, and supports advanced probabilistic reasoning principles for reasoning about complex probability distributions induced by concurrent threads, e.g. tape presampling and induction by error amplification. The integration of these strong reasoning principles is highly non-trivial due to the combination of probability and concurrency in the language and the complexity of the Foxtrot model; the soundness of the logic relies on a version of the axiom of choice within the Iris logic, which is not used in earlier work on Iris-based logics. We demonstrate the expressiveness of Foxtrot on a wide range of examples, including the adversarial von Neumann coin and the $\mathsf{randombytes\_uniform}$ function of the Sodium cryptography software library. All results have been mechanized in the Rocq proof assistant and the Iris separation logic framework.

cs.LO↗

arXiv2026

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)

Differential privacy is the standard method for privacy-preserving data analysis. The importance of having strong guarantees on the reliability of implementations of differentially private algorithms is widely recognized and has sparked fruitful research on formal methods. However, the design patterns and language features used in modern DP libraries as well as the classes of guarantees that the library designers wish to establish often fall outside of the scope of previous verification approaches. We introduce a program logic suitable for verifying differentially private implementations written in complex, general-purpose programming languages. Our logic has first-class support for reasoning about privacy budgets as a separation logic resource. The expressiveness of the logic and the target language allow our approach to handle common programming patterns used in the implementation of libraries for differential privacy, such as privacy filters and caching. While previous work has focused on developing guarantees for programs written in domain-specific languages or for privacy mechanisms in isolation, our logic can reason modularly about primitives, higher-order combinators, and interactive algorithms. We demonstrate the applicability of our approach by implementing a verified library of differential privacy mechanisms, including an online version of the Sparse Vector Technique, as well as a privacy filter inspired by the popular Python library OpenDP, which crucially relies on our ability to handle the combination of randomization, local state, and higher-order functions. We demonstrate that our specifications are general and reusable by instantiating them to verify clients of our library. All of our results have been foundationally verified in the Rocq Prover.

cs.PL↗

arXiv2026

All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs

Nondeterminism makes parallel programs challenging to write and reason about. To avoid these challenges, researchers have developed techniques for internally deterministic parallel programming, in which the steps of a parallel computation proceed in a deterministic way. Internal determinism is useful because it lets a programmer reason about a program as if it executed in a sequential order. However, no verification framework exists to exploit this property and simplify formal reasoning about internally deterministic programs. To capture the essence of why internally deterministic programs should be easier to reason about, this paper defines a property called schedule-independent safety. A program satisfies schedule-independent safety, if, to show that the program is safe across all orderings, it suffices to show that one terminating execution of the program is safe. We then present a separation logic called Musketeer for proving that a program satisfies schedule-independent safety. Once a parallel program has been shown to satisfy schedule-independent safety, we can verify it with a new logic called Angelic, which allows one to dynamically select and verify just one sequential ordering of the program. Using Musketeer, we prove the soundness of MiniDet, an affine type system for enforcing internal determinism. MiniDet supports several core algorithmic primitives for internally deterministic programming that have been identified in the research literature, including a deterministic version of a concurrent hash set. Because any syntactically well-typed MiniDet program satisfies schedule-independent safety, we can apply Angelic to verify such programs. All results in this paper have been verified in Rocq using the Iris separation logic framework.

cs.PL↗

arXiv2025

Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants

Although randomization has long been used in distributed computing, formal methods for reasoning about probabilistic concurrent programs have lagged behind. No existing program logics can express specifications about the full distributions of outcomes resulting from programs that are both probabilistic and concurrent. To address this, we introduce Probabilistic Concurrent Outcome Logic (pcOL), which incorporates ideas from concurrent and probabilistic separation logics into Outcome Logic to introduce new compositional reasoning principles. At its core, pcOL reinterprets the rules of Concurrent Separation Logic in a setting where separation models probabilistic independence, so as to compositionally describe joint distributions over variables in concurrent threads. Reasoning about outcomes also proves crucial, as case analysis is often necessary to derive precise information about threads that rely on randomized shared state. We demonstrate pcOL on a variety of examples, including to prove almost sure termination of unbounded loops.

cs.LO↗

arXiv2025

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)

We present Coneris, the first higher-order concurrent separation logic for reasoning about error probability bounds of higher-order concurrent probabilistic programs with higher-order state. To support modular reasoning about concurrent (non-probabilistic) program modules, state-of-the-art program logics internalize the classic notion of linearizability within the logic through the concept of logical atomicity. Coneris extends this idea to probabilistic concurrent program modules. Thus Coneris supports modular reasoning about probabilistic concurrent modules by capturing a novel notion of randomized logical atomicity within the logic. To do so, Coneris utilizes presampling tapes and a novel probabilistic update modality to describe how state is changed probabilistically at linearization points. We demonstrate this approach by means of smaller synthetic examples and larger case studies. All of the presented results, including the meta-theory, have been mechanized in the Rocq proof assistant and the Iris separation logic framework This is the extended version of the same paper accepted at ICFP 2025, where more details of proofs and case studies are included in the Appendix.

cs.LO↗

arXiv2025

Verified Foundations for Differential Privacy

Differential privacy (DP) has become the gold standard for privacy-preserving data analysis, but implementing it correctly has proven challenging. Prior work has focused on verifying DP at a high level, assuming the foundations are correct and a perfect source of randomness is available. However, the underlying theory of differential privacy can be very complex and subtle. Flaws in basic mechanisms and random number generation have been a critical source of vulnerabilities in real-world DP systems. In this paper, we present SampCert, the first comprehensive, mechanized foundation for differential privacy. SampCert is written in Lean with over 12,000 lines of proof. It offers a generic and extensible notion of DP, a framework for constructing and composing DP mechanisms, and formally verified implementations of Laplace and Gaussian sampling algorithms. SampCert provides (1) a mechanized foundation for developing the next generation of differentially private algorithms, and (2) mechanically verified primitives that can be deployed in production systems. Indeed, SampCert's verified algorithms power the DP offerings of Amazon Web Services (AWS), demonstrating its real-world impact. SampCert's key innovations include: (1) A generic DP foundation that can be instantiated for various DP definitions (e.g., pure, concentrated, Rényi DP); (2) formally verified discrete Laplace and Gaussian sampling algorithms that avoid the pitfalls of floating-point implementations; and (3) a simple probability monad and novel proof techniques that streamline the formalization. To enable proving complex correctness properties of DP and random number generation, SampCert makes heavy use of Lean's extensive Mathlib library, leveraging theorems in Fourier analysis, measure and probability theory, number theory, and topology.

cs.CR↗

arXiv2025

Logical Relations for Formally Verified Authenticated Data Structures

Authenticated data structures allow untrusted third parties to carry out operations which produce proofs that can be used to verify an operation's output. Such data structures are challenging to develop and implement correctly. This paper gives a formal proof of security and correctness for a library that generates authenticated versions of data structures automatically. The proof is based on a new relational separation logic for reasoning about programs that use collision-resistant cryptographic hash functions. This logic provides a basis for constructing two semantic models of a type system, which are used to justify how the library makes use of type abstraction to enforce security and correctness. Using these models, we also prove the correctness of several optimizations to the library and then show how optimized, hand-written implementations of authenticated data structures can be soundly linked with automatically generated code. All of the results in this paper have been mechanized in the Coq proof assistant using the Iris framework.

cs.LO↗

arXiv2024

Approximate Relational Reasoning for Higher-Order Probabilistic Programs

Properties such as provable security and correctness for randomized programs are naturally expressed relationally as approximate equivalences. As a result, a number of relational program logics have been developed to reason about such approximate equivalences of probabilistic programs. However, existing approximate relational logics are mostly restricted to first-order programs without general state. In this paper we develop Approxis, a higher-order approximate relational separation logic for reasoning about approximate equivalence of programs written in an expressive ML-like language with discrete probabilistic sampling, higher-order functions, and higher-order state. The Approxis logic recasts the concept of error credits in the relational setting to reason about relational approximation, which allows for expressive notions of modularity and composition, a range of new approximate relational rules, and an internalization of a standard limiting argument for showing exact probabilistic equivalences by approximation. We also use Approxis to develop a logical relation model that quantifies over error credits, which can be used to prove exact contextual equivalence. We demonstrate the flexibility of our approach on a range of examples, including the PRP/PRF switching lemma, IND\$-CPA security of an encryption scheme, and a collection of rejection samplers. All of the results have been mechanized in the Coq proof assistant and the Iris separation logic framework.

cs.LO↗

arXiv2024

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs

Probabilistic programs often trade accuracy for efficiency, and thus may, with a small probability, return an incorrect result. It is important to obtain precise bounds for the probability of these errors, but existing verification approaches have limitations that lead to error probability bounds that are excessively coarse, or only apply to first-order programs. In this paper we present Eris, a higher-order separation logic for proving error probability bounds for probabilistic programs written in an expressive higher-order language. Our key novelty is the introduction of error credits, a separation logic resource that tracks an upper bound on the probability that a program returns an erroneous result. By representing error bounds as a resource, we recover the benefits of separation logic, including compositionality, modularity, and dependency between errors and program terms, allowing for more precise specifications. Moreover, we enable novel reasoning principles such as expectation-preserving error composition, amortized error reasoning, and error induction. We illustrate the advantages of our approach by proving amortized error bounds on a range of examples, including collision probabilities in hash functions, which allow us to write more modular specifications for data structures that use them as clients. We also use our logic to prove correctness and almost-sure termination of rejection sampling algorithms. All of our results have been mechanized in the Coq proof assistant using the Iris separation logic framework and the Coquelicot real analysis library.

cs.LO↗

arXiv2024

A Demonic Outcome Logic for Randomized Nondeterminism

Programs increasingly rely on randomization in applications such as cryptography and machine learning. Analyzing randomized programs has been a fruitful research direction, but there is a gap when programs also exploit nondeterminism (for concurrency, efficiency, or algorithmic design). In this paper, we introduce Demonic Outcome Logic for reasoning about programs that exploit both randomization and nondeterminism. The logic includes several novel features, such as reasoning about multiple executions in tandem and manipulating pre- and postconditions using familiar equational laws -- including the distributive law of probabilistic choices over nondeterministic ones. We also give rules for loops that both establish termination and quantify the distribution of final outcomes from a single premise. We illustrate the reasoning capabilities of Demonic Outcome Logic through several case studies, including the Monty Hall problem, an adversarial protocol for simulating fair coins, and a heuristic based probabilistic SAT solver.

cs.LO↗

arXiv2024

Tachis: Higher-Order Separation Logic with Credits for Expected Costs

We present Tachis, a higher-order separation logic to reason about the expected cost of probabilistic programs. Inspired by the uses of time credits for reasoning about the running time of deterministic programs, we introduce a novel notion of probabilistic cost credit. Probabilistic cost credits are a separation logic resource that can be used to pay for the cost of operations in programs, and that can be distributed across all possible branches of sampling instructions according to their weight, thus enabling us to reason about expected cost. The representation of cost credits as separation logic resources gives Tachis a great deal of flexibility and expressivity. In particular, it permits reasoning about amortized expected cost by storing excess credits as potential into data structures to pay for future operations. Tachis further supports a range of cost models, including running time and entropy usage. We showcase the versatility of this approach by applying our techniques to prove upper bounds on the expected cost of a variety of probabilistic algorithms and data structures, including randomized quicksort, hash tables, and meldable heaps. All of our results have been mechanized using Coq, Iris, and the Coquelicot real analysis library.

cs.LO↗