Dated notes, including the misses — nothing here claims more than the proof or test behind it.
2026-09-04
security
We red-teamed our own live contracts 2 fixed1 left open
Most of what we publish here is a proof or a benchmark. This one is closer to an audit finding — the kind we'd want a third party to write about us, except we found it first and it's on our own live testnet contracts.
We went back through BondedValidatorV3 / BondedJudgePanelV3 with a specific question: not "does this match its own spec" (Halmos already checks that) but "does it correctly assume how the chain underneath it actually behaves." Two real issues came out of that pass. Both are fixed and deployed. One turned out to be a calculation, not a bug, and we're leaving it open on purpose.
Fixed — judge votes had no secrecy
BondedJudgePanelV3's panel selection is commit-reveal protected — who becomes a judge can't be predicted in advance. But the votes themselves were not: voteVerdict recorded a judge's score immediately on submission. A judge voting third could see the first two votes before deciding their own. Kleros's and UMA's own designs both depend on voting without seeing each other's answers first — that's what a Schelling-point mechanism actually requires. We had copied the shape of that game theory without copying the part that makes it hold.
Fix:BondedJudgePanelV4 splits voteVerdict into commitVerdict (a hash of your vote) and revealVerdict (the real values, checked against your own commit) — reusing the exact pattern already used for panel selection.
Fixed — state updates happened after the external call
stake(), registerJudge(), and stakeMore() all called token.transferFrom(...) before updating internal balances — a checks-effects-interactions ordering violation. Not exploitable with our current test token, but the pattern opens a reentrancy window the moment a hook-bearing token is used. Fixed by writing state before the external call.
Investigated, not fixed — judge-pool capture cost
Our judge lottery weights veteran judges 5× a newcomer's draw odds. We computed the exact capture probability (full permutation enumeration, not a Monte Carlo estimate) for a colluding minority opening several independent cases and only using the ones that draw in their favor:
Pool size
Colluding share
P(capture)
Cost for 90% success
10
30% of veterans
5.0%
~405× fee
30
same
0.27%
~7,500× fee
100
same
0.014%
~148,000× fee
Not a code defect — a deployment-parameter question. Small, concentrated pools are cheap to capture; past ~30 diverse participants, they're not. Recorded as a deployment rule, not a fix.
v0.2.1 of our validator had a liveness gap: an agent locks bond on a claim, and the only release path is a judge's verdict — which only happens if someone pays to open a case. If nobody does, the bond locks with no expiry. We built a system whose stated purpose is bounded settlement time, and it had an unbounded path.
What we're building is not "a supply of challengers" — it's "an upper bound on how long anything stays locked." If nobody challenges, the claim settles unverified, not verified. We are not manufacturing that probability. We are only pricing it honestly.
That's LOCK-0 in our design doc, fixed before a line of Solidity, so we couldn't quietly redefine "settled" as "verified" once the design got harder.
What the closest prior systems do
UMA's Optimistic Oracle v3 and OP Stack's fault proofs both fund a supply of challengers by paying the loser's stake to the winner. We can't do that — our own economic theorem says a winner's reward is mathematically equivalent to a bribery subsidy. So the gap we're filling is specifically "an optimistic window with no winner's bounty" — which is also, honestly, our weak point: we have no mechanism that manufactures challengers.
What we built
settleUnchallenged — callable by anyone, no reward, no token movement — releases the bond once the challenge window closes unopened, tagged "unchallenged". Not a verdict; consumers must exclude it from anything counted as verified.
What this costs, honestly
Deterrence is conditional on q, the probability a false claim actually gets challenged. At q = 0.5 a hallucinating agent's residual bond stays above our own kill-criterion line — a disclosed weakness, not a hypothetical one.
Sources: exp30/EXP30.md §0, §2, §12.6 · live as BondedValidatorV3 0xd881d52F10220687297651DeC4d55C1644d3a2A7
2026-09-03
proofs
Our machine proof was vacuous
We machine-verify our contracts with Halmos, a symbolic execution tool that checks a property against every possible input in a stated state space. Getting a [PASS] feels like a strong claim. This week we found out one of ours wasn't real.
The property
We had a Halmos property asserting that once two judges agree on a score, a timeout-triggered settlement can never revert. It reported [PASS].
What Halmos actually checked
voteVerdict accepted a raw uint8 score with no upper-bound check, while the registry downstream requires ≤100. Two judges voting 101 makes the registry write revert — permanently. The bond locks with no code path out.
When a call reverts, Halmos discards that trace instead of flagging it, so a property phrased as "always returns ok" can pass by construction even when every real trace in the danger zone reverts. The concrete counterexample: s1 = s2 = 0x80 (128). It reverts, every time. The [PASS] wasn't lying about what it checked — it was vacuously true, because we asked the wrong question.
The fix
v0.3 rejects the vote at submission: require(score ≤ MAX_SCORE) inside voteVerdict itself, plus a tag-length cap closing an identical-shaped gas-griefing path found at the same time.
Why we're writing this down
The honest version of "we use formal methods" includes the times formal methods didn't save us. [PASS] is a claim about a specific formalization, not about the code. We'd rather publish the miss than let the green checkmark do more talking than the counterexample.