Your LLM Produces Strings. That's the Whole Problem.

Every LLM hands you back a string. Confident, fluent, plausible — and unverifiable. In a chat that’s fine. In science, engineering, or any pipeline where the reasoning matters more than the vibe, it’s the whole problem: you can log what the model did, you can ask it to explain itself, but you still can’t check that the answer follows from the evidence. Logging isn’t verification. Explanation isn’t verification. A second model agreeing isn’t verification.

Eigenius is an open-source attempt to fix this at the substrate level — a verification layer where AI-produced claims carry their derivations and are mechanically checked, not taken on trust. Under the hood it’s dependent type theory, proof-carrying claims, and a way to compose reasoning across different domains without the meaning silently corrupting at the seams. In practice it means an AI result you can actually check: what was declared, what was observed, what was derived from what, and what was independently verified.

I’ll show it running end to end, walk through where it catches things that pass every format check and are still wrong, and talk about what’s hard about building this — including the parts that aren’t working yet. It’s open source; the goal of the talk is as much to find people to break it and build on it as to present it.