Darwin's Machines: How do we assess the risk of AI?
From exam-gaming models to speciation and military embodiment — a map of AI risks, how we might assess them, and why mitigation is harder than it looks.
Blog
Insights, tutorials, and updates on high-assurance AI systems, neuro-symbolic programming, and vericoding.
From Vibecoding to Vericoding: A Gradient, Not a Jump
You do not have to go from zero to verified in one step. You can start with Gherkin scenarios, graduate to executable contracts with specsaver, and then bring in a theorem prover when you are ready. Contracts are the bridge.
Understanding Software in the Large: Contracts and Compositionality
A top-level contract tells you what a system does. Sub-contracts tell the prover how it does it. You only need to read the first one. This is componentisation in real terms — and it changes how we think about software at scale.
The Cost of Correctness: Why Formal Verification Is About to Get Cheap
seL4 took 20 person-years to verify 8,700 lines of C. CompCert produced zero compiler bugs under extensive fuzzing. The guarantees have always been worth it. The cost has not. AI changes that.
Proof as Commodity
We proved type preservation for PCF — a classic typed lambda calculus benchmark — using two frontier LLMs and rocq-piler. DeepSeek v4 completed it in 21 minutes for $0.06. Claude Opus 4.8 took 14 minutes for $6.80. Either way, mechanised proof is no longer expensive.
Code Will Become Opaque — And That's Fine
Most software developers haven't twigged the real potential of automated theorem proving with LLMs. If provers are powerful enough, you no longer need to understand the code — only the contracts at the interface.
Axiomander: Robots on Rails
Contracts as plain assert statements. Verification via Coq and SMT. Zero imports, zero decorators, zero runtime overhead. Bringing theorem-prover-grade verification to real Python programmers.
Which Model Should Verify Your Extractions? A Cost-Quality Analysis of LLM Checkers
Every extraction pipeline needs a verification step. We tested eight models as quality scorers and found that for hallucination detection, a model costing 200× less than Claude performs identically. But for events, model quality still matters.
Why a Structured Ontology Beats a Flat Notepad for LLM Short-Term Memory
Giving an LLM a typed, navigable knowledge structure instead of a flat scratchpad changes what it can remember, how it updates facts, and how much context it consumes doing so.
How Do You Measure an LLM's Memory? Precision and Recall for Conversation Facts
String matching cannot tell you whether an LLM remembers what was said in a conversation. We describe the QA-probing methodology we use to measure short-term memory recall and wiki precision, and what our first results reveal.
Ghost Entities: Why LLM Hallucinations in Entity Extraction Are a Serious Downstream Risk
Hallucinated entities and relationships look identical to real ones inside a knowledge graph. We measured how often frontier models inject facts from parametric memory rather than from your documents — and found rates as high as 73% on a single document. Here is why that matters and what to do about it.
Which LLM Finds People Best? Benchmarking Claude, GPT-5.4 and Gemini 3 on PERSON Entity Extraction
We ran three frontier models on 8 open-licence documents and measured how accurately each one identifies named people — before and after cross-checking. The results reveal meaningful differences in hallucination rates and the value of verification.
Self-Prompt Injection: The Security Threat Nobody Is Talking About
You sanitized all your user inputs. Your prompt template is static. You think you're safe from prompt injection. You're not — and the attack vector is the agent itself.
No posts match your filters.