Jonathan Woollett-Light

York, United Kingdom • +44 7941 079483 • jonathanwoollettlight@proton.me
github.com/JonathanWoollett-Lightlinkedin.com/in/jonathan-wlYouTube

I am a PhD student in Physics at the University of York, working on neuromorphic computing for resource-efficient autonomous systems; my thesis is titled ‘Are SNNs more robust?’. This entails investigation of a wide range of AI/ML/RL algorithms and their respective hardware accelerators with particular focus and consideration of neuromorphic hardware and algorithms, and how they compare to more traditional ANNs. I have a specific interest in low level systems and tooling. I am a frequent Open-Source contributor having contributed to ziglang, rustlang and popular Rust crates. I have a small educational YouTube channel where I very infrequently post videos about technical topics I find interesting (A little more than an introduction to – YouTube).

Experience

York UniversityApril 2025 – Current

PhD in Physics

I am currently undertaking a PhD in Physics at the University of York with an idea of a thesis on how spiking neural networks (SNNs) interact with robustness; with the broad thrust of the thesis being to provide a more encompassing answer to the question of whether SNNs are more robust than ANNs.

In my exploration of the literature and initial experimentatation I went through multiple iterations of thinking I’d found a novel contribution only to find it had been already done (to varying extents). Through struggling to find an unexplored area, I considered work on contribution of a novel methodology re-running existing experiments under a more structured and equal framework, although I came to think that this claim of a contribution of a novel methodology to justify publication of questionably novel results would seem a strategy of masking a failure to find a truly novel contribution rather than a real contribution to be proud of. In continuing my reading I have tried to focus on narrow, falsifiable claims, eventually settling on an ablation study on the leak and reset paramters of leaky-integrate-and-fire (LIF) neurons in SNNs, analyzing their recurrence properties and how they interaction with different forms of perturbation.

Amazon Web ServicesApril 2022 – June 2024

Cambrigde – Software development engineer

I worked on Firecracker, a memory efficient, fast booting VMM that allows AWS lambda to be profitable.

Firecracker supports snapshotting a VM; a VM can be saved and restored much faster than booting a new one and much faster than any other VMM. I spent time working on the safety and configurability of this feature, this involved evaluating whether a snapshot could be safely restored on a given CPU considering its specified features and security mitigations, and those of the target. This involved analysis of the performance and security effects of CPU features on both x86-64 and aarch64, and ensuring we had an implementation that aligned with the specifications.

Firecracker supports a feature called CPU templates that allows a user configurability of most of how the CPU is presented to the guest OS. This work required understanding the Intel x86-64, AMD x86-64 and Arm aarch64 specifications. Development involved thorough discussion with customers and within our team both focused on usability, security and robustness. I rewrote how Firecracker handles static CPU templates to support runtime CPU templates and wrote the foundational implementation for runtime CPU templates. I also implemented thorough compatibility checks for x86-64.

I was the owner of an initiative to performance test Firecracker in production-like scenarios, through this we discovered and fixed significant performance regressions that may have costed AWS Lambda millions of dollars if they went live. This work involved coordinating across teams and diving deep into the deployment and management of resources to setup the required environment and execute the useful tests.

In this role I and another team member adopted responsibility for maintenance of the rust-vmm open source organization that maintained components used by Firecracker and other VMMs such as cloud-hypervisor.

RenishawJuly 2018 – September 2018

Wotton-under-Edge – Software placement

I worked on building C++ components forming an internal standard library. This involved extensive testing and performance consideration.

RenishawA few weeks in 2016

Wotton-under-Edge – Work experience

My work experience focused on development with FPGAs and VHDL.

Education

Swansea University2017 – 2021

MEng Computing & Bachelors 2.1

I competed with the university Taekwondo society, at times internationally.

Brighton and Hove Sixth Form College2015 – 2017

A levels – Mathematics: B, Modern History: B, Computer Science: C

I did an Extended Project Qualification discussing the question ‘Is the development and completion of an AGI (Artificial General Intelligence) likely within the next 80 years?’.

St Andrew’s High School2011 – 2015

GCSEs 11 A*–C including mathematics and english

I founded the computing club, the debating club and was elected deputy head boy by students.

Portfolio

I am an expert in Rust, I am experienced in C++, C and Python, and I am familiar with Zig, Ada, aarch64 asm, RISC-V asm, JavaScript and CSS3+HTML5.

My programming language: A verifying compiler for bare-metal RISC-V, written in Rust. You write a small Python-like language, and the compiler accepts your program only if it can prove (by symbolically executing the actual machine code across every hardware-thread interleaving and every admissible type assignment) that no assertion can fail and no memory access is ever out of bounds, even for intentionally racy, lock-free code. Its type inference is complete, or ‘infallible’: a variable left unspecified is accepted exactly when some typing makes the whole program verify, because inference and verification are the same search. The proof’s by-products then drive code generation: it infers the memory layout and performs dead-data elimination, deleting interior bytes of live data it proved are never touched at runtime and rewriting the address arithmetic to match. It verifies the instructions themselves rather than high-level source, shrinking the trusted base to a small layout-only lowering plus the assembler and linker; conceptually it generalises Zig’s concrete compile-time evaluation to full symbolic exploration and turns Rust’s conservative data-race prohibition into exact, per-assertion race verification, with parallel and distributed (MPI) verifiers checked against a trusted single-threaded oracle. (source)

CV website: A simple website serving the latest version of my curriculum vitae. Written in LaTeX and rendered to a single self-contained page: a near-perfect Google Lighthouse score, light and dark mode support, less than 100kb in size, and neatly prints to PDF.

Property search: A rental property search tool that scrapes Rightmove and ranks listings against weighted preferences for distance, price, size and ‘vibe’, the last elicited by pairwise voting scored with Glicko-2. It is a single self-contained HTML page with no backend: floor area is read out of the floorplan image by Moondream2, a vision-language model running in the browser through Transformers.js and WebGPU, falling back to Tesseract OCR where WebGPU is unavailable, and the location box autocompletes offline from a bundled GeoNames dataset of UK places. It is tested by driving the real, unmodified page in a headless browser over WebDriver with the network intercepted, so the whole user journey is deterministic and each run records screenshots, a trace and logs.

Hearts of Iorn 4 modding: I’m the owner and contributor to multiple Hearts of Iron 4 mods on the Steam Workshop (OWB – The Think Tank and Millennium Dawn: A Modern Day Mod). Working with mods and the often non-technical people making them requires a uniquely scrappy approach to development and a lack of hangups on formal processes (being able to work within what might politely be described as a mess), certainly a mindset shift from my traditional systems development.

Dating app: A dating app that learns user specific traits and preferences to match pairs. The server functions as an efficient monolith capable of handling all requests on a single Rust Axum server with in-memory stores and a local SQL store, achieving near 100% system utilisation capable of handling millions of users; supporting all the functionality of a typical tinder-like dating app.

CI Metrics: A website to track performance metrics (continuous benchmarking) and integrate with GitHub. A Rust Axum backend with a MongoDB database. Development focussed on experimentation with algorithms for anomaly detection to produce a solution that accomplishes what AWS Lookout for Metrics does, but at a much lower cost and complexity. This was motivated by my experience working on Firecracker at AWS where regressions that could have cost millions in production were almost missed, and certainly some were.

Live migration web server: A Rust server framework where a new server process can succeed a local old process in milliseconds with shared memory (or remotely in seconds over TCP) without dropping client streams. This can be used as a database server with in-memory data storage akin to Redis where queries are compiled as new functions.

RUST-AD: Auto-differentiation library with code transformation for both forward and reverse auto-diff written in Rust.

Mathematics Site: A mathematics website for automated marking. Built with a Rust Actix backend using a PyTorch semantic segmentation model, deployed with AWS, with a MongoDB database.

GLSL BLAS: GLSL code for non-complex BLAS operations with Vulkan. My final year masters project. Using modern C++ compile-time evaluation to validate shaders.

BLAS website: A website documenting BLAS operations. While working on GLSL BLAS I found the older website used to document BLAS to be a little uncomfortable, so I made this. I’ve also added some Python Manim animations to illustrate the operations.

Cogent: A simple library Rust library using ArrayFire for training simple neural networks; like a small Keras. A component of my final year bachelors project.

Genetic Draughts AI: My first ever venture into machine learning and optimisation. A simple tree C++ search program to play draughts using a genetic algorithm to judge board positions. I still remember the moment it beat me.