Hello David,
TL;DR: let me take responsibility for two Omarchy components
Omarchy has more than 5,000 open issues and pull requests. I’m offering to take responsibility for the menu and lock-screen backlog: investigate reports, consolidate duplicates, compare competing PRs, prepare fixes and keep their verification current as upstream changes. In my October 15 inventory, Proof classifies 234 open issues and 230 open PRs as fully within that scope. That is 464 items, about 8.5% of the open backlog, before counting work that overlaps other components. Once the process and me get enough trust, my ambition to take over bigger part on verification in Omarchy project. I have did a lot of review and triage already
In the last year I dedicated myself on software verification in agentic era, and building software factories. I have exact plan how to add determinism and trust to the process, and fix the backlog without loosing control over the vision. I wrote many time to Omarchy team, and to all public emails, and have not got an answer, so this is one more attempt to bring attention.
You keep the product vision. We agree on what those components must do and what must remain true. I use Proof to turn that agreement into versioned requirements, executable checks and deterministic acceptance rules. Fixes that satisfy the agreed rules can proceed under delegated authority. Missing or failed checks go back for engineering work; changes to the experience, disputed intent and exceptions come to you or the responsible maintainer with evidence and a concrete question. That is how I intend to reduce your decision queue to work that actually needs your judgment.
Start small, earn trust, then expand. Judge the process on those two components: whether bugs are resolved, fixes hold up, and maintainers spend less time reconstructing the investigation. Other contributors can take responsibility for other areas under the same rules. I have already started building and running this with Proof; the examples below show the verification and the infrastructure behind it.
Why I’m offering
I was the weird guy who enjoyed recompiling the Gentoo kernel and watching videos in ASCII. I love this stuff.
I started my own web consultancy in 2005, building with Rails 0.10. Since then, I’ve created or been a core contributor to open-source projects with 40,000 GitHub stars combined. I also helped rsync’s maintainers triage hundreds of issues for the 3.5.0 release, working through reports, tests, competing fixes and the cases that needed their judgment.
I’ve dedicated myself to software verification and to how our engineering craft needs to evolve as agents do more of the implementation. I want to put that work to use here: take responsibility for real components, make the results inspectable, and earn the trust to do more.
The problem I want to take off your hands
On August 21, you set a goal for Omarchy’s growing backlog:
“Goal is sub-100 issues/PRs at any time.”
By September 12, you were asking for help with triage: 2,200 open PRs, nearly a hundred arriving each day. Your follow-up drew the boundary: you would keep control of the user experience, while contributors consolidated competing PRs, removed duplicates and got work ready for consideration.
I responded by reporting bugs, investigating them and submitting patches. From the community triage channel, I still cannot tell who owns an investigation through to resolution or how it reaches the core team. I would like to help make that path explicit.
As of October 15, there are 3,194 open pull requests and 2,244 open issues. You later described the backlog as a river of suggestions, and some should be rejected or deferred. But a bug that violates agreed behavior does not need a new decision about the product’s direction. If a fresh prompt inherits an old delete confirmation, a contributor can fix that failure and demonstrate that the surrounding behavior is preserved.
The plan has two parts: define and check the boundaries of a correct change, then operate the intake, investigations and verification across a repository that keeps moving. Here is what that looks like in practice.
Follow one fix from the patch to its proof
Take my Omarchy JSONC parser PR, #13968. The old parser could remove commas inside strings, corrupting labels or shell commands. Other inputs could empty the menu or create phantom entries. A fix needs to handle those failures without changing valid menu content.
There are three connected records you can inspect:
The Omarchy PR: the parser change, documentation and 36 new regression assertions. The PR records 16 assertions that fail on the baseline and 20 that protect behavior it already gets right.
The public Proof PR: a draft verification mirror of that candidate, with four added requirements, their failure analysis, requirement-linked witnesses, scanner MC/DC cases and an additional 3,000-input comparison against a separately implemented reference model. The original issue reproducers remain as regression checks. This mirror is not a second patch intended for upstream merge.
The portal review of the exact PR: affected requirements, observed results, changed behavior and unresolved questions. It also flags when the baseline changes and the review needs refreshing.
The additional 3,000-input check compares parsed root-entry IDs across strings, comments, commas, array roots and varied whitespace. That is extra verification retained in the Proof fork, alongside the focused upstream contribution. Both records identify the revisions they concern; an old result cannot approve today’s changed branch.
Where the required tests come from
“Remove trailing commas” leaves too much unsaid. Requirement SW-REQ-260927-66FW in the Proof PR states the rule precisely: drop a comma if and only if it is outside a string and the next relevant character closes an object or array. “Relevant” means after skipping whitespace and line comments.
Those two conditions give us this truth table of required behavior:
The linked test block contains seven assertions covering all four input combinations. Multiple examples cover details the Boolean table alone cannot express: escaped quotes, end-of-input, and a comment between the comma and closing bracket. That last case exposed a failure in a competing patch.
This is how I answer “how many tests are enough?” For this rule, we can enumerate the combinations and attach witnesses to each. The parser also needs input-domain checks, failure cases and MC/DC over its implementation decisions. Four rows do not prove the whole parser correct. They make one part of the verification obligation exact, so a reviewer can see what is covered and what still needs evidence.
The linked requirement is my proposed specification in the Proof fork, not an upstream-approved product decision. Establishing that authority is part of the process I’m proposing.
What does “correct” mean here?
For the menu and lock screen, I started by recovering requirements from the code, documentation and existing reports. What should happen when a new menu request arrives? What must remain unchanged? Which actions are destructive? What happens when a password, command or configuration is malformed?
Recovered requirements start as candidate interpretations. Maintainers establish which ones have authority. Once agreed, the same requirement can guide many contributors and agent sessions. An unclear or disputed requirement comes back for a decision; a routine fix inside that agreement does not need the product question reopened.
Some questions have an obvious investigative answer. I can demonstrate that an old dialog consumed a new request’s keystroke. Others need a decision: should a destructive uninstall action ever be the default search result? How long should an authentication attempt remain valid after the screen goes blank? I can explain the alternatives and their consequences. An agent should not quietly choose one and call every other behavior a defect.
Historical proposal, 5 October 2026: establish a component baseline before reviewing changes. The counts describe that snapshot; 19 of the 71 findings used static source checks rather than runtime reproduction. Requirements were draft interpretations awaiting maintainers; solver checks concern the encoded model, not every ambiguity in natural language. MC/DC applies to measured targets, not the entire desktop.
Proof organizes the requirements into user goals, system behavior and software obligations, with links to the relevant implementation and checks. That gives a change a boundary. A parser fix should satisfy its intended requirement while preserving the menu behaviors around it. If an agent changes those behaviors too, the review needs to say so.
Formalizing a requirement makes it possible to ask questions that prose alone tends to hide. Can the conditions ever occur? Can two requirements be satisfied together? Does the formal statement actually express the intended behavior? The last question still requires judgment; a solver can check a model without knowing that I modeled the wrong thing.
A requirement with explicit checks. The JSONC requirement’s formal statement, linked test and MC/DC rows. These rows describe the formula; they are not themselves test pass/fail results. The same view keeps stale review and six open known issues visible beside a recorded machine pass. Inspect the record ↗
I then use Proof to examine failure cases such as malformed input, boundaries, timing and interrupted operations. Those create specific testing obligations. MC/DC adds another question: has each condition independently changed the outcome of its decision? Behavioral comparisons run the old and new implementation on the same inputs and make differences visible.
That gives any contributor a concrete way to answer “have I tested enough?” The obligations, supporting evidence and remaining gaps are explicit. It does not produce a magic test count that proves an entire desktop correct. The formal model has assumptions, comparisons cover executed inputs, and some behavior requires the actual desktop environment.
A maintainer should be able to see those limits without reading the agent’s entire conversation.
Put deterministic checks around the agents
Running two or three Codex agents does not establish an acceptance rule. They can all agree on a patch while missing the same requirement, or generate tests that repeat the implementation’s mistake. More opinions cannot substitute for an explicit account of what must remain true.
Proof connects that account to executable checks and a versioned record of the change. The aim is to make as much of acceptance as possible deterministic. For the same recorded inputs, evidence and policy, the gate should reach the same decision without asking another model whether the answer looks convincing.
That means concrete rules:
The requirement has an identity and a version. A worker can propose changing a requirement. That change must pass the approval policy before it can redefine success for the patch.
The evidence names what ran and what it checked. Test output, a counterexample or a solver result is distinct from an agent saying the code looks right.
The result belongs to exact revisions. A pass from an earlier patch or an affected baseline cannot stand in for verification of the current change.
Required checks are enforced. A failed or missing obligation blocks the acceptance path that requires it. Waiving it needs explicit authority and a recorded reason.
Changes are checked against the recorded obligations. A fix must preserve the agreed surrounding behavior, or expose the proposed requirement change for a decision.
The boundaries need engineering too. A deterministic check can enforce the wrong requirement, and a test suite can miss a dependency. Models help recover intent, propose checks and find counterexamples; maintainers settle consequential questions. The formal properties and executable checks then constrain subsequent work. This is how a useful judgment becomes something the next agent has to respect.
For a timing-sensitive desktop bug, the environment and schedule also matter. Reproducible runs, controlled inputs and explicit uncertainty are more useful than pretending the whole execution is deterministic. The rules for accepting the evidence should still be explicit.
I have already compared the competing fixes
The same JSONC parser PR also shows how this process helps resolve competing contributions.
Several reports and patches touched related failures. A trailing-comma expression could alter text inside strings, including shell commands. A root array could become menu entries named 0 and 1. An inline comment could empty the menu. Fixing those separately produced overlapping changes and additional cases to compare.
I brought the investigation together and compared my parser with #13681 on 200,000 generated documents. The PR also records preservation of the shipped menu’s 344 rows and their data. It identifies a combination of trailing comma, comment and closing brace that other candidate patches missed. The description includes the comparison script so someone else can examine the result.
It also contains a mistake of mine. Greptile caught a Unicode whitespace problem in the first version. I fixed it and kept the expanded inputs for later comparisons. My October 5 architecture proposal records how they exposed a related whitespace regression in #6525.
That is the improvement I care about. A review finding becomes a check that relevant later work has to face. The next review should inherit that check without depending on someone remembering the corner case.
I also offered to carry the necessary changes and tests into the competing PR if that was the version the team preferred. The result matters more than which contributor’s branch gets merged.
A completed review can still need another check. The JSONC PR review retains its evaluated revision and observations, while flagging a re-check after the proof baseline moved. This is evidence for a particular revision, not a current blanket approval of the PR. Captured on 15 October 2026. Inspect the record ↗
The other open contributions illustrate different obligations: #14155 checks how accented application names sort, including the ordering tradeoffs; #14153 checks that the menu offers theme removal only when the underlying action has a removable theme. These are small pieces of an explicit account of how the component should behave.
The infrastructure has to keep up
Building this factory is some of the hardest engineering I’ve worked on. The requirements, checks and evidence have to stay tied to the intended behavior and the code being evaluated, while the repository keeps changing underneath them. I’ve spent a substantial amount of time on that problem: running the fleet, assigning work, handling failures and deciding when an earlier result has stopped being useful.
A good investigation in one chat is still fragile. Someone has to notice the next report, connect it to the existing defect, assign the work, check the answer and revisit it when the code changes.
The portal keeps an inventory of issues and pull requests, including their revisions, current state and relevant relationships. Reports can point to one underlying defect. Several patches can be related, competing or complementary. A changed report is retained as a revision rather than silently replacing the text an earlier judgment relied on.
Proof first classifies which reports belong to the area I am investigating, before spending compute on reproduction and audits. Starting with the menu and lock screen makes the scope manageable and gives me a concrete basis for evaluating that classification. Items outside that scope remain visible for someone else to investigate.
Start with the part we can take responsibility for. The operator inventory separates menu and lock-screen work from the wider repository. These are scope classifications, not confirmed bugs. One failed classification remains visible. Counts are a snapshot from 15 October 2026.
The next work is explicit: confirm the area, investigate a duplicate, connect a report to a known issue, compare a PR, reproduce a proposed defect, or refresh an earlier review. Workers claim particular items. Claims expire if a worker disappears, and a late result from an obsolete claim cannot overwrite the current work. When the underlying facts change, the affected work opens again.
These mechanisms have to work together. A worker can disappear halfway through a review. Another can return after the PR has changed. Two agents can investigate different versions of the same report. Scaling the fleet means handling those cases without making a maintainer reconcile every conversation by hand.
Give each piece of work an owner and a way to recover. Real work claims show the task, agent, heartbeat, lease and retry. A silent worker is visible instead of silently losing its task. “Completed” counts tasks, not fixed bugs. This is the operator view, captured on 15 October 2026.
Tasks also need the right environment. A metadata worker cannot reproduce a desktop interaction. Concurrency limits, retries, budgets and pause controls keep failed or interrupted work manageable without someone watching every terminal.
The same system has to follow upstream. An evaluation belongs to particular code and assumptions. New PR commits can require a new review. A change to the audited baseline can affect several candidates. Evidence can be retained where its basis still holds; uncertain impact triggers another check. An old green result should not silently become a claim about a new revision.
The agents need checking too
On the parser PR, two upstream agents disagreed about whether the change was a bug fix or an enhancement, so execution stopped pending a maintainer. I can keep investigating the behavior while that classification is unresolved, then bring you the decision with the comparisons already done. Product authority stays with you; the investigation does not have to start again after you answer.
I use separate workers and model families to challenge proposals too. But agreement is not a measurement of accuracy. The infrastructure can replay previously decided cases as hidden controls and track later staff corrections. The known-answer evaluation has no samples yet, so I still need to establish how reliably those reviewers work. Executable evidence remains separate from their opinions.
Preparing that evidence also does not give every worker permission to post comments or decide what Omarchy should merge. Those actions have their own permissions.
I have done this work beyond Omarchy
I helped with rsync’s 3.5.0 release, working with the maintainers on issue triage, tests, PR reviews and the difficult distinction between a security defect and expected behavior. rsync is a widely used Linux and Unix utility with a C codebase going back to 1996. Changes there have consequences well beyond the repository.
The Proof audit filed 99 findings. Its public record also includes 28 later withdrawals, and fixes from the work shipped in 3.5.0. Keeping that investigation useful through a moving release meant correcting conclusions as the evidence changed and working through the cases that required maintainer judgment.
That experience is relevant here. A queue of agent-generated findings is easy to produce. Taking responsibility for the investigation, the corrections and the path to a release is the work I want to scale.
Share the work within explicit boundaries
Oligarchy and ThePrimeagen’s work with agents in virtual machines show that Omarchy is building its own automation. I can contribute the requirements, verification and fleet-management machinery I have been building. That work can support more people taking responsibility, with a common record of what each change must preserve and what has actually been checked.
The public Omarchy project in Proof shows where I have started. It supports investigating incoming reports, reviewing other people’s PRs and preparing fixes. Each useful result should improve the next investigation: a clearer requirement, another reproducer, a missing test case or a review rule that would have caught my last mistake.
Adapted from the 5 October 2026 proposal. A finding becomes a retained check; upstream changes trigger work where recorded dependencies overlap. Added checks cover more cases, not every future defect. File-level impact matching was automatic; a finer row-level decision in the example was recorded by hand.
David, I would like to take responsibility for the menu and lock-screen backlog. Agree on the behavior, required checks, permissions and escalation path with me, and I will own the investigation through to a verified fix or an explicit decision. The queue, evidence and unresolved questions should be visible to the team.
You keep ownership of Omarchy’s experience. Within the agreed boundaries, contributors can carry fixes through under explicit acceptance and merge permissions. Product changes, unresolved questions and exceptions come back to the responsible maintainer with evidence.
Judge the process by how much investigation maintainers no longer have to repeat, how well the conclusions survive scrutiny and how much work reaches a defensible outcome. Start with the components already modeled, then expand as the process earns trust.
That is how I think we can make the backlog manageable without making you the bottleneck for every bug fix.
Lets fix everything!