arXiv subjects

Sebastian Ertel

Publications and source records attributed to Sebastian Ertel.

8 recordsLinked to original sources

arXiv2026

Corten - Foundational Verification of Rust Programs

We present Corten, a foundational verification framework for Rust programs in the Rocq theorem prover, built on the Iris separation logic framework. Corten provides the first semantics of surface-level Rust mechanized in a proof assistant with an attached program logic, directly grounded in the Rust Reference: it deeply embeds the Typed High-level Intermediate Representation (THIR) into Rocq and formalises Rust's dynamic semantics as a weakest-precondition predicate transformer calculus. By operating at THIR rather than on internal compiler representations, Corten proof goals display the THIR AST, which pretty-prints to surface Rust, keeping verification close to the source code and facilitating maintainability as code evolves. Atop this semantics, Corten develops a program logic and a syntax-directed proof automation layer; the program logic includes defunctionalized continuation stacks that keep proof goals first-order and compact. Soundness is established incrementally, construct by construct, against an interaction-trees denotation. A synthetic test suite demonstrates a two-to-four times reduction in proof size compared to raw semantic proofs. We further showcase Corten on a buddy allocator case study, verifying memory safety of the allocation and deallocation functions, laying the groundwork for end-to-end verification in a shared Rocq semantic foundation spanning hardware-software boundaries.

cs.PL↗

arXiv2026

NoC-Out: A Formally-verified Network-on-Chip Library for Rule-based Hardware Designs

The Network-on-Chip (NoC) is the communication backbone of any multiprocessor chip. A failure of the NoC has severe consequences for the whole system. Yet, no approach exists that provides formally-verified NoCs with strong guarantees but without tedious verification effort. Any library that generates formally-verified NoCs needs to be parametric in the structure of the NoC. This requires a hardware description language (HDL) that allows for parametric and concurrent yet efficient hardware designs as well as the necessary program logic to reason about them in a modular fashion. So far, HDLs fall short in both aspects. In this paper, we implement NoC-Out, the first library/generator for formally-verified k-dimensional NoC designs. In order to build NoC-Out, we extended K\^oika, a rule-based HDL in the Rocq theorem prover, with support for concurrent yet efficient NoC designs and a program logic for modular, automated reasoning. Given a configuration, NoC-Out produces a k-dimensional torus NoC in K\^oika, which can then be compiled to Verilog. Each produced NoC is equipped with a proof that it refines our formal NoC specification; no additional verification effort is required. Our specification proves a strong liveness guarantee, which consequently applies to all generated NoCs. In our evaluation, we find that our verification approach is even required to synthesize efficient NoCs in rule-based HDLs.

cs.PL↗

arXiv2026

Harnessing Code Agents for Automatic Software Verification

Formal verification offers the strongest guarantee of software correctness, but it does not scale: the proofs demanded by interactive theorem provers such as Coq require enormous expert effort. Large language models (LLMs) promise to generate these proofs automatically, yet existing approaches wire a fixed, human-designed proof strategy into the system and constrain the model to follow it (retrieving premises and predicting tactics one step at a time, or splitting goals by divide-and-conquer), and still prove only a fraction of their target theorems. We show that imposing such a strategy is unnecessary and limiting. Handing the whole lemma to a general LLM code agent (for example, Claude Code), free to choose its own approach, and wrapping it in a verification harness is both simpler and more effective, achieving full coverage: every targeted lemma proved, with no failures and no Coq expert intervention. The agent writes the proofs under feedback and hard constraints from the harness that keep each one sound (accepted only when the prover's kernel closes it), complete (no obligation left unproved or silently dropped), and terminating (no divergent tactics). We evaluate this harness plus code agent along three dimensions. (1) Core logic: on Iris, the state-of-the-art separation logic for concurrent and memory-manipulating programs, Aria proves all 4,257 lemmas of the four core modules and the 217 lemmas verifying Rust's standard libraries built on it, fully automatically. (2) Comparison with prior LLM provers: on reglang, where prior provers manage barely one in eight, Aria proves all 318. (3) Generality: on iris-lean, the unfinished Lean 4 port of Iris, it proves 72 not-yet-ported lemmas, showing the approach is not specific to Coq. A state-of-the-art model (Claude Opus 4.7) can write proofs for verified software development fully and automatically.

cs.FL↗

arXiv2026

Interaction Tree Semantics for RISC-V: Bridging Compiler and Hardware Verification

The Instruction Set Architecture (ISA) is the contract between compilers and processors; proving this contract formally demands cross-level connection to existing mechanized compilers and hardware implementations. As an open, modular ISA gaining adoption across embedded, mobile, and cloud platforms, RISC-V makes a formally verified ISA specification particularly valuable. However, existing formal RISC-V specifications focus on hardware tooling rather than cross-level verification: they provide no machine-checked instruction-level properties and lack support for verifying this contract across levels. We address these limitations with a formal semantics of the RISC-V ISA in Rocq, built on Interaction Trees (ITrees). By leveraging ITree bisimulation and refinement, our semantics enables cross-level verification from compiler IR to hardware within a single framework. Our formalization covers a wide spectrum of RISC-V extensions. The correctness of individual instruction semantics is backed by machine-checked lemmas in Rocq. We further validate it by extracting an executable simulator that passes all standard RISC-V test suites. Three case studies demonstrate the effectiveness of our semantics for cross-level verification: first, we prove semantic equivalence via bisimulation between LLVM IR and RISC-V code on an array access pattern via Vellvm (LLVM ITree semantics); second, we apply translation validation to a specific instruction reordering for macro-operation fusion, distinguishing safe reorderings from those that break program-counter-relative addressing; third, we prove that a K\^oika hardware ALU correctly implements all R-type integer operations (e.g., ADD, SUB, AND) against our ISA contract.

cs.PL↗

arXiv2025

Formally-verified Security against Forgery of Remote Attestation using SSProve

Remote attestation (RA) is the foundation for trusted execution environments in the cloud and trusted device driver onboarding in operating systems. However, RA misses a rigorous mechanized definition of its security properties in one of the strongest models, i.e., the semantic model. Such a mechanization requires the concept of StateSeparating Proofs (SSP). However, SSP was only recently implemented as a foundational framework in the Rocq Prover. Based on this framework, this paper presents the first mechanized formalization of the fundamental security properties of RA. Our Rocq Prover development first defines digital signatures and formally verifies security against forgery in the strong existential attack model. Based on these results, we define RA and reduce the security of RA to the security of digital signatures. Our development provides evidence that the RA protocol is secure against forgery. Additionally, we extend our reasoning to the primitives of RA and reduce their security to the security of the primitives of the digital signatures.

cs.CR↗

arXiv2023

On the mean field theory of Ensemble Kalman filters for SPDEs

This paper is concerned with the mathematical analysis of continuous time Ensemble Kalman Filters (EnKBFs) and their mean field limit in an infinite dimensional setting. The signal is determined by a nonlinear Stochastic Partial Differential Equation (SPDE), which is posed in the standard variational setting. Assuming global one-sided Lipschitz conditions and finite dimensional observations we first prove the well posedness of both the EnKBF and its corresponding mean field version. We then investigate the quantitative convergence of the EnKBF towards its mean field limit, recovering the rates suggested by the law of large numbers for bounded observation functions. The main tool hereby are exponential moment estimates for the empirical covariance of the EnKBF, which may be of independent interest. In the appendix of the paper we investigate the connection of the mean field EnKBF and the Stochastic Filtering Problem. In particular we derive the Feedback Particle Filter for infinite dimensional signals and show that the mean field EnKBF can viewed as its constant gain approximation.

math.PR↗

arXiv2022

Analysis of the Ensemble Kalman--Bucy Filter for correlated observation noise

Ensemble Kalman--Bucy filters (EnKBFs) are an important tool in Data Assimilation that aim to approximate the posterior distribution for continuous time filtering problems using an ensemble of interacting particles. In this work we extend a previously derived unifying framework for consistent representations of the posterior distribution to correlated observation noise and use these representations to derive an EnKBF suitable for this setting as a constant gain approximation of these optimal filters. Existence and uniqueness results for both the EnKBF and its mean field limit are provided. The existence and uniqueness of solutions to its limiting McKean-Vlasov equation does not seem to be covered by the existing literature. In the correlated noise case the evolution of the ensemble depends also on the pseudoinverse of its empirical covariance matrix, which has to be controlled for global well posedness. These bounds may also be of independent interest. Finally the convergence to the mean field limit is proven. The results can also be extended to other versions of EnKBFs.

math.PR↗

arXiv2019

Category-Theoretic Foundations of "STCLang: State Thread Composition as a Foundation for Monadic Dataflow Parallelism"

This manuscript gives a category-theoretic foundation to the composition of State Threads as a Foundation for Monadic Dataflow Parallelism. It serves as a supplementary formalization of the concepts introduced in the Article "STCLang: State Thread Composition as a Foundation for Monadic Dataflow Parallelism", as published in Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell (Haskell'19).

cs.PL↗