Insights, tutorials, and updates on high-assurance AI systems, neuro-symbolic programming, and vericoding.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.