Writing
Research notes, engineering write-ups, and tutorials on the verification, security, and privacy of AI.
Research Notes
The questions and observations behind the work, from a single paper to connections across several.
October 2026Data That Only One Model Can Read
Adversarial examples exploit what a model notices; non-transferable examples use what it does not. How data can remain useful to a designated model without being equally useful to other models.
October 2026What Makes a Hull Approximation Useful
Why exact local bounds can still lose joint information, and how the useful precision of an approximation depends on the property and the work needed to use it.
October 2026Why Linear Bounds Lose Cancellation When They Are Summed
A valid bound for every activation can still produce a weak bound for their sum. The missing information is how their approximation errors move together.
October 2026Why Nonlinear Substitution Has to Stay Local
Quadratic symbolic bounds preserve useful structure, but composing them across a network would make polynomial degree explode. Locality is the scalability contract.
September 2026What Gradients and Embeddings Can Reveal
A comparison of reconstruction risks in collaborative training and vector retrieval, and what GRAB, GHOST, and SHAQ change.
September 2026Where Control Enters: Weights, Updates, Outputs, and Data
Four places to intervene in the use of models and data, and the different assumptions behind CoreLocker, AdaLoc, AIM, and non-transferable examples.
January 2026Why Reusing ReLU's Own Pieces Makes Hull Approximation Cheap
Over-approximating the ReLU convex hull is expensive because the hull is hard to describe. Reusing the function's own linear pieces as the lower faces turns the construction into bookkeeping over edges and vertices.
Engineering Notes
Why a representation, an interface or an implementation is designed the way it is.
January 2026Activation Hulls: What Makes an Approximation Sound?
The containment contract behind activation-hull approximations, why a sampled hull is not enough, and how the maintained wraact library exposes constraints.
January 2026ShapeONNX: Solving ONNX's Dynamic Shape Problem
A dual-track shape inference tool that resolves ONNX's dynamic shapes to concrete static values for neural network verification workflows.
January 2026SlimONNX: A Story of Optimizing Neural Networks for Verification
A pure Python toolkit for optimizing ONNX models specifically for verification workflows, validated on the VNN-COMP 2024 benchmark suites.
January 2026TorchONNX: A Compiler for ONNX-to-PyTorch Conversion
ONNX is already an explicit graph, so compiling it does not make it readable -- it makes it directly consumable by the PyTorch tooling that can analyze it. Why the compilation is worth doing, and what the intermediate representation is actually for.
January 2026TorchVNNLIB: A Story of Fast VNN-LIB Property Loading
How a VNN-LIB specification becomes ordered tensors and arrays that keep its logical grouping, so a benchmark with thousands of properties is not re-parsed on every run and a property file can be deserialised instead of parsed.
NNV Guide · A series in progress
A Guide to Neural Network Verification
Understand what a verifier proves, how bounds and relaxations work, and where their guarantees end.
29 guides · 4 parts · Foundations to advanced topics
- 01
Foundations
7What a verifier is asked to prove, and what its answer means.
- 02
Methods & Tools
10How bounds, relaxations and solver pipelines turn that question into constraints.
- 03
Practice
6Specifications, benchmarks, and the testing that complements a proof.
- 04
Advanced Topics
6Where verification gets expensive, and which architectures and defenses answer it.
Every article is also listed on the article archive, by date. That is the archive; this page is organised by what each piece is for.