We report on the development of an optimized and verified decision procedure for orthologic equalities and inequalities. This decision procedure is quadratic-time and is used as a sound, efficient and predictable approximation to classical propositional logic in automated reasoning tools. We formalize, in the Coq proof assistant, a proof system in sequent-calculus style for orthologic. We then prove its soundness and completeness with respect to the algebraic variety of ortholattices, and we formalize a cut-elimination theorem. In doing so, we discover and fix a missing case in a previously published proof.

We then implement and verify a complete proof search procedure for orthologic. A naive implementation is exponential; to obtain an optimal quadratic run time, we optimize the implementation by memoizing its results and simulating reference equality testing. We leverage the resulting correctness theorem to implement a reflective Coq tactic. We present benchmarks showing that the procedure, under various optimizations, matches its theoretical complexity.

Finally, we develop a collection of tactics, including normalization with respect to orthologic and a boolean solver, which we also benchmark. We make tactics available as a standalone Coq plugin.

Systems code is challenging to verify, because it uses constructs (like raw pointers, pointer arithmetic, and bit twiddling) that are hard for tools to reason about. Existing approaches either sacrifice programmer friendliness, by demanding significant manual effort and verification expertise, or generality, by restricting the programming language or requiring that the code adapt to the verification tool.

We identify a new point in the design space of verifiers that enables a different set of trade-offs, which prove practical in the context of verifying critical system-components. We use several novel techniques to develop the TPot verification framework, targeted specifically at systems code written in C. With TPot, developers verify critical components they implement in standard, unrestricted C, using a C-based language to write “proof-oriented tests” (POTs) that specify the desired behavior. TPot then runs the POTs to prove correctness. We evaluate TPot on 6 different systems-code bases, and show that it can verify them at the same level as 4 state-of-the-art verifiers, while reducing the annotation burden by a factor of 1.36-3.46x. TPot does not require these code bases to be adapted for verification and achieves verification times compatible with typical continuous-integration workflows.

The process isolation enforceable by commodity hardware and operating systems is too weak to protect secrets from malicious code running on the same machine: Spectre-era attacks exploit timing side channels derived from contention on shared microarchitectural resources to extract secrets. With appropriate hardware support, however, we can construct isolated enclaves and safeguard independent processes from interference through timing side channels, a necessary step towards integrity and confidentiality guarantees.

In this paper, we describe our work on formally specifying and verifying that a synthesizable hardware architecture implements strong timing isolation for enclaves. We reason about the cycle-accurate semantics of circuits with respect to a trustworthy formulation of strong isolation based on “air-gapped machines” and develop a modular proof strategy that sidesteps the need to prove functional correctness of processors. We apply our method on a synthesizable, multicore, pipelined RISC-V design formalized in Coq.

Modern software needs fine-grained compartmentalization, i.e., intra-process isolation. A particularly important reason for it are supply-chain attacks, the need for which is aggravated by modern applications depending on hundreds or even thousands of libraries. Object capabilities (ocaps) are a particularly salient approach to compartmentalization, but they require the entire program to assume a lack of ambient authority. Most of existing code was written under no such assumption; effectively, existing applications need to undergo a rewrite-the-world migration to reap the advantages of ocap. We propose gradual compartmentalization, an approach which allows gradually migrating an application to object capabilities, component by component in arbitrary order, all the while continuously enjoying security guarantees. The approach relies on runtime authority enforcement and tracking the authority of objects the type system. We present Gradient, a proof-of-concept gradual compartmentalization extension to Scala which uses Enclosures and Capture Tracking as its key components. We evaluate our proposal by migrating the standard XML library of Scala to Gradient.

We present an executable, proven-safe, faithful, and future-proof Coq mechanization of JavaScript regular expression (regex) matching, as specified by the last published edition of ECMA-262 section 22.2. This is, to our knowledge, the first time that an industrial-strength regex language has been faithfully mechanized in an interactive theorem prover. We highlight interesting challenges that arose in the process (including issues of encoding, corner cases, and executability), and we document the steps that we took to ensure that the result is straightforwardly auditable and that our understanding of the spec aligns with existing implementations.

We demonstrate the usability and versatility of the mechanization through a broad collection of analyses, case studies, and experiments: we prove that JavaScript regex matching always terminates and is safe (no assertion failures); we identify subtle corner cases that led to mistakes in previous publications; we verify an optimization extracted from a state-of-the-art regex engine; we show that some classic properties described in automata textbooks and used in derivatives-based matchers do not hold in JavaScript regexes; and we demonstrate that the cost of updating the mechanization to account for changes in the original specification is reasonably low.

Our mechanization can be extracted to OCaml and linked with Unicode libraries to produce an executable engine that passes the relevant parts of the official Test262 conformance test suite.

Modern regex languages have strayed far from well-understood traditional regular expressions: they include features that fundamentally transform the matching problem. In exchange for these features, modern regex engines at times suffer from exponential complexity blowups, a frequent source of denial-of-service vulnerabilities in JavaScript applications. Worse, regex semantics differ across languages, and the impact of these divergences on algorithmic design and worst-case matching complexity has seldom been investigated.

This paper provides a novel perspective on JavaScript's regex semantics by identifying a larger-than-previously-understood subset of the language that can be matched with linear time guarantees. In the process, we discover several cases where state-of-the-art algorithms were either wrong (semantically incorrect), inefficient (suffering from superlinear complexity) or excessively restrictive (assuming certain features could not be matched linearly). We introduce novel algorithms to restore correctness and linear complexity. We further advance the state-of-the-art in linear regex matching by presenting the first nonbacktracking algorithms for matching lookarounds in linear time: one supporting captureless lookbehinds in any regex language, and another leveraging a JavaScript property to support unrestricted lookaheads and lookbehinds. Finally, we describe new time and space complexity tradeoffs for regex engines. All of our algorithms are practical: we validated them in a prototype implementation, and some have also been merged in the V8 JavaScript implementation used in Chrome and Node.js.

We present verification of a bare-metal server built using diverse implementation techniques and languages against a whole-system input-output specification in terms of machine code, network packets, and mathematical specifications of elliptic-curve cryptography. We used very different formal-reasoning techniques throughout the stack, ranging from computer algebra, symbolic execution, and verification-condition generation to interactive verification of a compiler for a C-like language. All these component specifications and domain-specific reasoning techniques are defined and justified against common foundations in the Coq proof assistant. Common between these components is a minimalistic specification style based on functional programs operating on simple objects, omnisemantics for program execution, and assertions in simple separation logic. This design enables us to bring the components together in a top-level correctness theorem that can be audited without understanding or trusting the internal interfaces and tools. Our case study is a simple cryptographic server for flipping of a bit of state through authenticated network messages, and the proof about it shows total functional correctness including static bounds about memory usage. We believe it is the first formal verification covering a full software stack that models both network input and output. This paper also describes our experiences with the specific verification tools we build upon, along with detailed analysis of reasons behind the widely varying levels of productivity we experienced between combinations of tools and tasks.

There are typically two ways to compile and run a purely functional program verified using an interactive theorem prover (ITP): automatically extracting it to a similar language (typically an unverified process, like Coq to OCaml) or manually proving it equivalent to a lower-level reimplementation (like a C program). Traditionally, only the latter produced both excellent performance and end-to-end proofs.

This paper shows how to recast program extraction as a proof-search problem to automatically derive correct-by-construction, high-performance code from purely functional programs. We call this idea relational compilation — it extends recent developments with novel solutions to loop-invariant inference and genericity in kinds of side effects.

Crucially, relational compilers are incomplete, and unlike traditional compilers, they generate good code not because of a fixed set of clever built-in optimizations but because they allow experts to plug in domain–specific extensions that give them complete control over the compiler's output.

We demonstrate the benefits of this approach with Rupicola, a new compiler-construction toolkit designed to extract fast, verified, idiomatic low-level code from annotated functional models. Using case studies and performance benchmarks, we show that it is extensible with minimal effort and that it achieves performance on par with that of handwritten C programs.

Automated verifiers rely on SMT solvers as a backend for proof automation. This simplifies verification in the common case, but also creates usability challenges due to instability. Previous work proposes mitigation strategies motivated by the assumption that instability is a fundamental theoretical limitation. We conjecture that the instability experienced by verifiers today is often caused by fixable engineering problems, and is thus not fundamental. Should this be true, the more consequential approach to addressing instability would be to identify root causes and connect them with solver improvements.

We conducted case studies on 11 deemed-unstable queries from existing verification projects and from issues reported on the Z3 repository, with the goal of diagnosing the root causes of instability. For all of them, instability is attributable to solver bugs, misconfigurations, or misaligned expectations. We present our analysis and draw conclusions regarding better instability metrics, interfaces that make instability explicit, systematic debugging methods, and easier-to-debug SMT solvers.

Highly automated theorem provers like Dafny allow users to prove simple properties with little effort, making it easy to quickly sketch proofs. The drawback is that such provers leave users with little control about the proof search, meaning that the small changes inherent to the iterative process of writing a proof often lead to unpredictable variations in verification time, and eventually hard-to-diagnose proof failures. This sometimes turns the boon of high automation into a curse, as instead of breaking early and showing unsolved goals to the user like in Coq, proofs tend to gradually become unstable until their verification time explodes. At this point, the absence of a proof context to investigate often leaves the user to a painful debugging session. In this paper, we show how to use Dafny modules to encode Coq-like induction principles to dramatically improve the stability and maintainability of proofs about inductive data structures.

Diagrams are ubiquitous in the development and presentation of proofs, yet surprisingly uncommon in computerized mathematics. Instead, authors and developers rely almost exclusively on line-oriented notations (textual abbreviations and symbols). How might we enrich interactive theorem provers with on-the-fly visual aids that are just as usable? We answer this question by identifying a key challenge: designing declarative languages for composable diagram templates, that provide good-looking implementations of common patterns, and allow for rapid prototyping of diagrams that remain stable across transformations and proof steps.

The process isolation enforceable by commodity hardware is too weak to protect secrets from malicious code running on the same machine: Spectre-era attacks have exploited timing side channels derived from contention on shared microarchitectural resources to extract secrets. We describe our work in progress on specifying and verifying strong timing isolation for synthesizable hardware. We reason about the cycle-accurate semantics of circuits with respect to a trustworthy formulation of strong isolation based on “air-gapped machines” and develop a modular proof strategy that sidesteps the need to prove functional correctness of processors. We demonstrate our method on a multicore, pipelined, RISC-V design formalized in Coq. Finally, we discuss future directions toward composing isolation guarantees with speculative, constant-time guarantees to obtain a software-to-hardware, end-to-end guarantee of timing side channel freedom.

All critical systems must evolve to meet the needs of a growing and diversifying user base. But supporting that evolution is challenging at increasing scale: Maintainers must find a way to ensure that each change does only what is intended, and will not inadvertently change behavior for existing users. This paper presents how we addressed this challenge for the Amazon Web Services (AWS) authorization engine, invoked 1 billion times per second, by using formal verification. Over a period of four years, we built a new authorization engine, one that behaves functionally the same as its predecessor, using the verification-aware programming language Dafny. We can now confidently deploy enhancements and optimizations while maintaining the highest assurance of both correctness and backward compatibility. We deployed the new engine in 2024 without incident and customers immediately enjoyed a threefold performance improvement. The methodology we followed to build this new engine was not an off-the-shelf application of an existing verification tool, and this paper presents several key insights: First, rather than prove correct the existing engine, written in Java, we found it more effective to write a new engine in Dafny, a language built for verification from the ground up, and then compile the result to Java. Second, to ensure performance, debuggability, and to gain trust from stakeholders, we needed to generate readable, idiomatic Java code, essentially a transliteration of the source Dafny. And third, to ensure that the specification matches the system's actual behavior, we performed extensive differential and shadow testing throughout the development process, ultimately comparing against one quadrillion of production samples prior to deployment. Our approach demonstrates how formal verification can be effectively applied to evolve critical legacy software at scale.

This paper lays out a case study of Software Construction, a new course in the undergraduate computer and communication sciences curriculum at EPFL. We hope to share some generalizable lessons we learned from running its first edition in Fall 2023. The course targets three core concepts—functional programming, real-world engineering, and correctness—and its design is informed by four principles—students should learn by doing, assignments should be self-motivating, knowledge should be built incrementally, and students should see progress over time. We illustrate how we realized these concepts and principles with practical examples of course materials and teaching methods that we hope will serve as useful inspiration to others teaching similar courses. Lastly, we present some encouraging preliminary data about course outcomes and share our speculations about experiments for its future evolution.