Insights, tutorials, and updates on high-assurance AI systems, neuro-symbolic programming, and vericoding.
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.
We built a simulated world and watched AI agents spontaneously develop survival instincts, form alliances, and spread their "genes." The pieces for an AI catastrophe aren't coming. They're already here.