I investigate cases where a computational system reports success without establishing the property that actually matters. I am an independent researcher and direct OMEGA, a computational research and verification system using AI-assisted investigation, independent checks and explicit evidence boundaries. How AI agents are used is set out below.

People act on green results. In the cases below, a solver answered sat where unsat was expected, a battery model's lithium inventory drifted by 2.44%, and a replay verifier said VERIFIED while a 100,000-byte write ran under a 4,096-byte cap.

Approved, not yet merged: Qcodes #8627, a numpy integer overflow fix for parameter stepping.

Reported and fixed by maintainers: inspect_ai #4602 and inspect-robots #413. LemmaScript #206 led to an opt-in impure marker on externs; the default is unchanged.

Under review: cedar-spec #995 (changes requested), Strata #1448, Strata-CLI #7 and #8, genome-nexus #881, chemprop #1417, TorchIO #1536.

Withdrawn: lean-kernel-arena #196 and #207. I closed both after a maintainer's question showed they added nothing the arena did not already have.

All merged PRs · all open PRs · all issues

Each repository has its own statement of limits.

• mcp-authority-boundary: the VERIFIED case above. The first version passed 66 tests and its ledger replayed cleanly, while an independent observer saw the oversized file. Its recorded reproductions are on my own machine and a GitHub-hosted runner. It covers one MCP server and one authored policy set, and the failure class (CWE-436) is not new.
• vsf-cjson: an experiment in how far an AI agent can port a C library to Lean 4, with unmodified cJSON as the oracle. It found four cJSON bugs, such as 1e400 parsing to null. Round-trip theorems are proved; which inputs the parser accepts is measured, not proved.
• inspect-replay: compares two Inspect AI evaluation logs sample by sample and reports "not recorded" separately from "unchanged".
• collective-bound and commons-agent-lab: the formal and empirical sides of an AMLUCS 2026 accepted poster. With caps summing to 1.5 times the shared budget and agents unable to see the pool, every agent stayed within its own cap and the budget was still breached in 60 of 60 baseline episodes on each of three models. commons-agent-lab is a preregistered study of a simplified environment, not a claim about deployed systems. The formal work in collective-bound was not preregistered, and its README records no known independent reproduction.
• spcu-verification: a small power-control IP checked with open formal tools. Two of five injected defects passed every property written from the specification, and 93 of 200 sampled netlist mutations survived and were observable.
• silent-pass-catalogue: 12 cases of a check passing after its property had failed, each with a reproducer and an upstream acknowledgement or independent oracle. They come from my own work, so no rate follows from them.

I designed and direct OMEGA. AI agents, including Claude, Codex and Cursor, carry out implementation, test development and execution, and much of the research and drafting. Commits and PRs under my name include this agent work, and commit metadata does not consistently record it. I choose what to investigate, set the acceptance criteria and stopping conditions, challenge the conclusions, and decide what the evidence justifies claiming.

Results that fail or narrow the original idea stay in the record.

The contributions above touch SMT solving, battery modelling, hardware verification and AI evaluation. Each is one specific result, not a demonstrated general capability in that field.

More: omegaprotocol.org