Fourth year Computer Science undergraduate at St Catherine's College, University of Oxford.
Formal Verification, Compilers, Hardware, Systems Security, Decompilers
Oxford Email: louis-emile dot ploix at stcatz dot ox.ac.uk
Personal Email: louisemile dot ploix at gmail dot com
GitHub: mndstrmr
In summer 2023, at Oxford, I formally proved that each 'event' of the CHERIoT-Ibex core was 'correct' with respect to the CHERIoT-RISC-V Sail specification, by compiling the spec to a SystemVerilog module and comparing.
Then in summer 2024 lowRISC invited me to generalise my proof for vanilla Ibex. In so doing I extended that proof to total trace equivalence, showing that in each case the specification and the implementation would produce the same sequence of memory operations in the same order, forever.
In summer 2025 I returned to lowRISC once more, where I brought my proof to work with entirely open source tooling (using slang, yosys-slang, yosys and rIC3), in addition to the commercial tools we were already using. See here. I also verified in Lean 4 that the properties proved by the model checker together imply trace equivalence of outputs. See here.
Feb 2025 – arXiv paper – Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor
Feb 2025 – Press releases – From lowRISC, and from the Oxford Department of Computer Science
Jul 2025 – Conference talk at DVClub Zurich – Proof Strategies in the Comprehensive Formal Verification of the Ibex Processors – (Audio gets better after a little bit)
Oct 2025 – Conference talk at Osmosis Europe – Formally Verifying Security Properties of CHERI Hardware and Software
Oct 2025 – Conference talk at DVClub World – Reproducing a Proof of Specification Compliance for Ibex with Open Source Tools
Dec 2025 – Conference talk at DVClub Cambridge – Crossing the Model Checking-Theorem Proving Gap for Ibex Correctness
Jan 2026 – LowRISC blog post on Open Source Formal – Open Source Correctness Proof for Ibex
Mar 2026 – Our formal work cited as central for CHERI certification of CHERIoT-Ibex – Announced at CHERI Blossoms 2026
From late 2025 to present I have been formally proving end-to-end correctness (equivalent to what we did for CHERIoT-Ibex) of the larger CHERI-CVA6 application core as a part of the COSMIC project with lowRISC. The verification code is not yet public.
Mar 2026 - CHERI Blossoms Conference Talk - COSMIC Verification - Comprehensive, end-to-end formal proofs of CVA6-CHERI (full YouTube video)
Jul 2025 – Source code (~20KLOC of Rust) for decompiler developed for 3rd year project – rdcp: A decompiler for Rust binaries
Feb 2025 – CatzExchange (non-technical audience) – Design and Large Scale Formal Verification of Modern Embedded Microprocessors
Oct 2025 – CompSoc CTF Introduction – Binary Exploitation and Reverse Engineering
Nov 2025 – CompSoc Member Talk – Formal Verification for Processor Cores
Jan 2026 – CompSoc Member Talk – The Decompilation Problem
Feb 2026 – CatzExchange (non-technical audience) – The Decompilation Problem