You're pledging to donate if the project hits its minimum goal and gets approved. If not, your funds will be returned.
AI agents run shell, git, file and API tools on real systems. Right now, the only thing stopping them from doing damage is the model behaving, which breaks under jailbreaks. qedra sits in the tool-call path and blocks the dangerous actions (force-pushing a protected branch, rm -rf, leaking a secret, wiping CI) without trusting the model at all. The z3 theorem prover checks the git policy, so it can prove it has no holes. Every session also produces a signed receipt anyone can verify with just a public key. It is already built, MIT-licensed, and I tested it on 3,790 real commands from 49 popular repos with zero false blocks and every attack I tried blocked. Honest scope: only the git core is Z3-proven; the other rules are high-precision heuristics, and the zero-knowledge receipts are still experimental.
What are this project's goals? How will you achieve them?
Goal: a trusted, adopted, deterministic control-and-audit layer for AI agents. Over 6 months, I will:
- Extend the blocked-action coverage past git to infra and data actions, tested the same way (zero false blocks on real commands, with a regression suite).
- Pay for an independent external review of the z3 policy and the receipt cryptography (the zero-knowledge part is experimental and needs outside eyes).
- Integrate it into 2-3 open-source agent frameworks (OpenHands, Aider, Continue) and get real users.
- Write up the threat model and a reproducible test harness.
I know it worked if coverage grows while false blocks stay at zero, the review is done, and at least one real framework is using it.
Total USD 40,000 for 6 months solo: about 65% my stipend (tax included), 15% the independent security review, 10% software and compute, 10% buffer. At the 10,000 minimum, I fund the independent review plus a part-time runway to broaden coverage and land the first framework integration.
Just me. I work in formal methods and applied cryptography: Coq and TLA+ proofs, Groth16 and Nova SNARKs, on-chain BLS (EIP-2537), and a from-scratch Rust layer-1. I recently built and open-sourced epbs-formal, a machine-checked TLA+/Coq verification of an Ethereum consensus change (EIP-7732), now submitted to the Ethereum Foundation. Honest note: I have not won a grant yet, and qedra's numbers come from replaying real commands, not live production deployments. What I can show is a working public repo you can run yourself (./verify.sh reproduces the validation) and a habit of shipping deep verification work alone.
- Adoption is the real risk. A guardrail only matters if frameworks integrate it. If nobody adopts it, it stays a good tool nobody uses. I am mitigating by shipping as a standard MCP server and writing the integration PRs myself.
- Coverage past the z3-proven git core is heuristic. Broadening it without creating false blocks is genuine work and could stall.
- The verifiable-receipt and ZK layer needs independent cryptographic review before anyone should trust it. If the review finds problems, that part gets cut back to what is proven, which still leaves a useful tool.
Zero so far, all self-funded. I applied to the Long-Term Future Fund (EA Funds) for this project on 2026-07-29, currently pending. My separate epbs-formal project is under review at the Ethereum Foundation ESP. No money is committed from anyone yet.