Skip to content
View repowazdogz-droid's full-sized avatar
2 followers · 0 following

Achievements

Achievement: Pull Sharkx2Achievement: Pair Extraordinairex2Achievement: YOLO

Achievements

Achievement: Pull Sharkx2Achievement: Pair Extraordinairex2Achievement: YOLO

Block or report repowazdogz-droid

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Content in all repositories owned by your account will be closed.
Maximum 250 characters. Please don’t include any personal information such as legal names or email addresses. Markdown is supported. This note will only be visible to you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
repowazdogz-droid/README.md

Warren Smith

I investigate cases where a computational check says everything is fine, but the property it is supposed to establish has already failed.

One experiment replayed as VERIFIED while executing a 100,000-byte write under a 4,096-byte cap.

That has taken me from agent authorization and formal verification to scientific software and hardware verification. I tend to build the smallest experiment I can that could prove my idea wrong, then keep the result even when it does.

AI assistance

I use AI heavily in this work, including Claude, Codex and Cursor for code, research and drafting; the commit history makes that visible. I choose what to investigate, set the tests and stopping conditions, and decide what the evidence justifies claiming. Results that fail or narrow the original idea stay in the record.

Selected work

Pinned below. If you read one, start with mcp-authority-boundary.

Reviewed upstream

Merged, mine: common_cells #355 (a SymbiYosys proof for the ECC encoder and decoder, which found an undriven syndrome_o), PyBaMM #5747 (a lithium-conservation fix in the Basic electrolyte model), inspect-robots #425 (records the effective grader configuration).

Reported here, fixed upstream: inspect_ai #4602, inspect-robots #413, LemmaScript #206.

Open: cvc5 #12937 (approved by a maintainer, awaiting merge), cedar-spec #995, Strata #1448, genome-nexus #881, and two in Strata-CLI.

All merged PRs · all open PRs · all issues

Contact

warren@omegaprotocol.org · omegaprotocol.org

Pinned Loading

  1. mcp-authority-boundary mcp-authority-boundary Public

    A Cedar-mediated MCP tool server whose v1 passed 66 tests and replayed as VERIFIED while writing 100,000 bytes under a 4,096-byte cap. The audit, the repair, and the independent observer that caugh…

    TypeScript

  2. spcu-verification spcu-verification Public

    A small power-control IP verified with open tools. Formal found four unseeded bugs; mutation analysis then showed two of five injected defects passed every property written from the specification.

    SystemVerilog

  3. safeguards-control-plane safeguards-control-plane Public

    A fault-injected Redis Streams testbed comparing a safeguard on the action path with one beside it. Beside it, the dashboard reported 1,026 actions prevented and all 1,026 executed.

    Python

  4. commons-agent-lab commons-agent-lab Public

    A preregistered study of 2,100 LLM-agent episodes on three models. Every agent stayed within its own allowance, yet the shared budget was breached in 60 of 60 baseline episodes per model. Four amen…

    Python 1 1

  5. capctl-iris capctl-iris Public

    A Rocq/Iris proof that a shared capability meter never exceeds its cap under any thread interleaving. 40 theorems, all closed under the global context.

    Rocq Prover

  6. evidence-audit evidence-audit Public

    Grades recorded Kani, loom and Lean outputs by what they explored, not the verdict they printed. Demonstrated on jsonwebtoken and governor, and on a Lean model that audits identically to a wrong one.

    Lean