Odeya

A research engine built on one refusal: never say more than you can prove. Question to contract to evidence to independent verification to bounded claim. Open, machine-verified, replayable.

Comment

Inspiration

Every lab today can generate answers. Almost none can show you, byte for byte, how an answer was produced, what failed on the way, and what is still unknown. I kept watching AI systems pass every benchmark and still fail on contact with reality, and I kept watching research tools delete their failures and tell a clean story. Odeya is my refusal of that: a research engine that will not say more than it can prove.

What it does

Odeya turns a research question into a governed, replayable chain: contract first, then work, then evidence, then independent verification, then a bounded claim. Nothing jumps the chain. Failures, nulls, and contradictions are first-class results that stay in the record forever. Models propose; a deterministic kernel governs. No model can grant itself authority, verify its own claim, or treat a provider response as truth.

The ecosystem

Odeya is not invented from an abstract agent demo. It is extracted from three open research missions that feed it real requirements, all under one account:

  • Sentinel ~ measurement discipline for autonomous-driving perception: runtime monitoring, failure localization, and transfer claims that stay bounded.
  • Telos ~ verifying autonomous agent work by evidence, not trust: published nulls, deliberately broken positive controls, and the finding that a verification repo can reward-hack its own guards.
  • Inbar ~ physical causal evidence: prospective intervention tests on real hardware, with proposal, safety, execution, truth, and publication authority kept separate.

Odeya is the architecture they all converge into: one engine where the whole chain of custody survives review.

How we built it

Architecture before engine, on purpose. The repository is 112 machine-verified JSON schemas, 47 recorded engineering decisions, 660 valid and adversarial cases across 12 isolated suites, bounded TLA+ models, and a validator that makes the repository prove its own claims on every clone. The core discipline: every gate ships with a known-bad proof that it actually fires. A check that cannot be shown to fail is not evidence.

Challenges we ran into

The hardest bugs were the flattering ones. My guard-coverage tool published five different coverage figures and every one was wrong in the direction that made the work look better; independent adversarial review caught all of them, I caught none. A migration tool silently "repaired" the deliberately wrong values inside eighteen known-bad fixtures, turning traps into decoration. Each failure became a law in the repo: measure by mutation, never trust green without a proof it can go red.

Accomplishments that we're proud of

The repository is live, public, and proving itself: green CI on every push, every commit reproducible from a fresh clone with retained rehearsal evidence. In one sustained push we drove the canonical-migration wave from 1,222 blocking findings to five of six classes measuring zero ~ every fixture timestamp pinned, every scientific decimal governed by a frozen typed contract, all 668 digest fields resolved to registered scopes ~ with each step recorded as a reviewable decision. And the engineering itself was AI-assisted: GPT/Codex and Claude sessions did the heavy lifting under my direction, and every line they produced had to survive the same validator, adversarial fixtures, and known-bad proofs as everything else. That is Odeya's thesis applied to itself: the discipline holds no matter who, or what, writes the code.

What we learned

Honesty is an engineering property, not a virtue. You can build a repository that is structurally unable to lie about itself, and once you have that, every claim on top of it gets cheaper to trust.

What's next for Odeya

The runtime is not built yet. That is the honest state and the design: the gates that keep an engine honest had to exist before the engine. Winning this gives me the fuel to build the engine inside the architecture that is already proven ~ clone it, run one command, and watch it prove itself: github.com/manfromnowhere143/odeya

Built With

  • claude
  • codex
  • formal-methods
  • github-actions
  • gpt-5.6
  • jsonschema
  • markdown
  • mermaid
  • node.js
  • openai
  • python
  • rfc-8785
  • sha-256
  • tla-plus
Share this project:

Updates

posted an update —

The tool is the smallest surface of a larger system, and the system moved.

Odeya, the CLI you can run in sixty seconds, audits one claim: that an agent's work is done. I built it small on purpose. It is one governed effect of a larger question I have been working toward. What should it take for an autonomous system to be allowed to act, when no test it can enumerate is proof it did the real work?

Two days since I submitted, the governed architecture behind the tool closed a problem worth stating plainly.

The repository records the finding first: a valid human signature is not a human decision. An authenticator proves a credential was exercised. It does not prove the person was shown the exact bytes they believe they approved. And binding the confirmation gesture to the signer is circular by construction, because the receipt names the challenge it belongs to, so a challenge that commits to the receipt commits to something that commits back to it.

The fix adds no trust. It removes the cycle by ordering. One phase commits to what was displayed and confirmed. A second phase commits forward to that receipt and never backward. Two independent implementations derive the same bytes, and a frozen reference vector still reproduces exactly, so the encoder is checked against its own past rather than against itself.

Stated as status, not as a caveat: this is a property of the construction, not evidence that any ceremony occurred. A presentation surface that lies about its own displayed bytes is detected when its receipt disagrees, never prevented. The acceptance gate is still closed. No engine runs yet.

Every claim here is one clone away. Published main is 34cad10. It carries 115 schemas, 93 decision records, 14 isolated contract suites where each gate ships a known-bad proof that it fires, 7 bounded formal models with 30 counterexamples, and 458 of 927 refusal statements proved load-bearing by mutation. The 469 still unproved are named, not rounded away.

The tool shows you the discipline in one command.

Log in or sign up for Devpost to join the conversation.