Arbiter Security
AI-native offensive security tools, built in Rust. Two products exposed as MCP servers: Arbiter (web-application vulnerability detection across 52 classes) and Aletheia (binary analysis across 14 CWE classes).
Exeter, UK · Founder, Arbiter Security
Laurence Avent
Security engineer building AI-native offensive tooling in Rust, with a sideline in reasoning a machine can re-check. I work where security engineering, language models, and formal verification meet.
Work
What I build
Tightrope Tracker
An open-source live dashboard of UK economic constraint, drawn from official OBR and ONS sources, with public methodology and codebase.
Security & AI tooling
Narsil-MCP (a 90-tool code-intelligence server), Forgemax (a V8 sandbox for LLM execution), Veilguard, Sanctum, and Krait.
Research
Reasoning that carries its own proof
A working system in which untrusted generators, language models among them, propose reasoning steps, a small kernel enforces the rules, and every accepted chain is re-checked byte-for-byte and re-proved in Lean 4. Its first case study is a determination of the van der Waerden number W(3,3); the papers and artifacts are on the research page.
Avent's Razor
Judge a reasoning system by the constraints it can enforce during search: enforcement prunes the space and, unlike insight, can be checked by machine.
Verified Chain-of-Thought
An 18-rule kernel, two independent byte-level checkers held to exact agreement, and a Lean 4 oracle that re-proves every step. Language models operate the loop through a typed gate.
W(3,3) = 27
Both directions machine-checked: a 382,964-step certificate covering the entire search, compiled to Lean and reduced to a single biconditional over colourings.
Contact
Get in touch
Open to conversations about security engineering, coordinated disclosure, and verified reasoning. Email is the fastest route.