Implemented BurnTracker and BurnTrackerTest with tests, real result fixtures, and deployment documentation.

• Build, formatting, and all 53 tests pass.
• Mainnet fork tests pass.
• The 4,545-byte update uses 266,914 execution gas.
• Callback storage/gas checks and runtime equality pass.

README documents launch parameters and operations. Mainnet deployment remains with IMD’s launch process; no transaction was broadcast.

I found no critical, high or medium defects in the economics. I've written two findings and a full coverage record to .imd-findings.json, and changed no project files. The test suite passes (53 of 53, fork tests excluded).

What holds:

• One order at a time: every path that places an order checks the state first. When the owner replaces a stale order, the old order's callback is refused afterwards.
• Payment: the live price is read before any token call. A price above maxPrice reverts before any tokens move. The caller is charged exactly the price, the Intake gets approval for exactly that amount, and nothing is left held or approved afterwards. Tokens sent to the contract by others stay untouched.
• Callbacks: they are accepted only from the Intake that took the awaited order, only for its requestId, only while PENDING, and only once. A bad ask from someone else that names this contract is refused, and callbacks move no funds.
• The 200,000-gas callback limit: callbacks write only two storage slots, the result hash and the packed progress slot. Both are nonzero from the constructor on, and a zero hash (or the starting placeholder hash) is rejected.
• The state rules match the brief exactly. That covers refusals, failures, staleness, recover and setResultHash.

The slither and aderyn leads don't hold:

• Reentrancy (slither): a single lock guards every external function.
• Strict equalities (slither): they compare state codes, so they are intended.
• "ETH transferred" (aderyn): the contract never sends ETH.

Findings:

1. Low: the owner can change what a keeper pays for, in the same block. A keeper is a third party who pays for the next update. When the keeper's updateBurntracker runs, it uses whatever intake, body and action are configured at that moment. The owner can submit setIntake, setBody or setActions ahead of it. For example, the owner front-runs with setIntake(E, IMD), where E quotes 0.5 IMD and sends the approved payment to the owner. The keeper's 0.5 IMD then goes to the owner and no job is ordered at the real Intake. maxPrice is the only limit on the loss. This comes from owner powers the brief requires, so it is low. The suggested fix keeps the interface: setter changes take effect only after a delay.
2. Info (outside the economics area): the constructor's two bytes arguments may not fit the launch manifest. The brief requires bodyPrefix and bodySuffix as constructor arguments. The launch recipe says each argument is a single 32-byte word, and bodySuffix is about 790 bytes. Whether the launch stops at the manifest depends on what the manifest step accepts, which I couldn't check.

All 26 entry points have a coverage row: 18 hold and 8 point to finding 1 (updateBurntracker and the three setters, on both contracts). Four invariant rows are added. The JSON parser and access control are other reviewers' areas, so I only spot-checked them.

The review is complete. .imd-findings.json holds five findings and thirty coverage rows, all snippets verified against the tree, and only that file plus test/scratch/ were touched.

Outcome. The permission model holds: every owner-only entry has onlyOwner, callbacks authenticate the original intake, the awaited request id and the PENDING state exactly once, updateBurntracker pulls only from its caller with maxPrice checked before any token touch, two-step ownership rejects zero and self, and the full 53-test suite passes. No permission bypass or fund-loss path was found in the Access Control, Trust Gap or Asymmetry guides. What I did find:

• Medium, deployability. The constructor takes two dynamic bytes parameters (16 and 721 bytes). The manifest rules allow one ABI word per entry and at most 16 entries. The real encoding is 35 words, and a nine-word static list fails to deploy in a scratch test. The README asserts the brief wins, but nothing shows the deployer can carry dynamic bytes. The fix is a scope decision: evidence the manifest accepts bytes, or seed the template from the already-compiled ContinuationTemplate library.
• Low, state trap. From STUCK after a failed update, an owner open() that the plane refuses drops to UNOPENED. There recover, setResultHash and updateBurntracker all revert, so the existing project is orphaned. Spec-literal, with a workaround through setActions, so reported for the author to decide.
• Low, owner literal. The tree hardcodes 0x887b... as "this launch's payer" though the brief named no address. The manifest must use $owner.
• Info, trust assumptions. The owner can redirect an in-flight keeper payment up to maxPrice by swapping the intake, and may open a second project from any stale or STUCK state. Both are intended owner powers, documented with reproductions.

Not covered. The assembly JSON extractor in ResultJson.sol is outside my area and marked unreached beyond the passing differential fuzz.

The review is complete. The findings file is at the repository root with 2 findings and 30 coverage rows, all entry points answered.

Area covered: Math Precision, Boundary, Numerical Gap. The contract has almost no arithmetic: uint40 timestamps with explicit overflow guards, inclusive 1 hour to 30 day timing bounds, a body-size bound that matches the order bound and the Intake's 16 KiB limit, and an inclusive maxPrice cap checked before any token read. All of those held at their exact boundaries in scratch tests. The real numerical work is the bit-parallel JSON scanner in ResultJson. I verified the byte-zero and control-character masks are carry-free, the quote-parity count is exact for up to 32 markers, the tail word is masked, and firstByte constants are correct. I then ran 210 Python-generated canonical documents (nested objects, unicode, escapes, jobId decoys, missing and duplicate keys) through the production parser, the repository's bytewise reference parser and Python's own expectation. All three agreed. Callback gas measured 35k to 42k of the 200k stipend across every transition, and the 4,545-byte update costs about 267k cold against the real mainnet bytecode replay.

Findings:

• Medium, launch boundary. The constructor takes two dynamic bytes parameters. Their encoding is 35 ABI words, while the evm_contracts manifest carries one static word per entry, at most 16, and no dynamic types. The README claims the brief overrides the recipe, but the manifest tool does not take that decision, so the launch may park after the build. I framed it as a policy conflict needing a decision, with a behaviour-preserving alternative: seed the template from the already-compiled ContinuationTemplate and keep setBody.
• Low, state machine seam. After a project exists, a failed update leaves STUCK, the owner may re-open, and if the plane refuses that open the contract returns to UNOPENED. From there neither recover nor setResultHash is reachable, so the only exit is another paid open that creates a new project. A failing Foundry proof is attached under test/scratch.

Not reached: nothing within the assigned area. The real Intake's callback encoding was checked only through the mock and the documented interface, since the fork test cannot run offline.

The review is complete and .imd-findings.json holds the result. The working tree is unchanged apart from the findings file and the ignored scratch test.

Outcome. The control flow of BurnTracker is sound in the areas I was assigned. I traced every state-changing entry point through its guards, state writes, external calls and failure paths against the Execution Trace, Periphery and First Principles checklists, and found no fund-loss or callback-authentication defect. The existing suite of 53 tests passes, including the gas-and-storage checks that run both callbacks under exactly 200,000 gas and confirm they write only two slots that are nonzero from construction.

Findings recorded (2):

• Medium, launch-blocking conflict. The constructor takes two dynamic bytes arguments for the template parts. The contracts-only launch recipe allows only one static word per manifest entry and no dynamic arguments. Encoding the nine documented arguments produces 35 words, so a nine-entry launch.json cannot deploy this contract. The brief does ask for these as constructor input, so I framed it as a policy conflict to confirm before the manifest step, with a remedy that seeds storage from the existing compiled template constants and keeps setBody owner-settable.
• Low, operational trap. open() is accepted from any STUCK or stale state, not only one produced by the hosting job. After a failed update, an owner re-open that the plane refuses drops the contract to UNOPENED. There, recover and setResultHash both revert, so the healthy hosted project cannot be continued until the owner pays for another successful opening. A scratch test under test/scratch/ reproduces the exact sequence.

Coverage. All 26 listed entry points have a row, plus rows for the constructor, three invariants, the parser and vendored libraries, and the static-analysis leads. Both BurnTrackerTest and BurnTracker share identical runtime, so the rows mirror each other. The owner's power to redirect future orders via setIntake is noted as a trust assumption, not a defect. The static-analysis reentrancy and ETH-transfer leads did not hold up on inspection.

Not reached. I did not run the online mainnet fork profile, and the real Intake's complete path was verified only through the mock and the offline bytecode replay, not a live call.

I added invariant tests and more failure-path tests for BurnTracker/BurnTrackerTest. The full suite passes with the verifier's fuzz seed: 68 tests across 8 suites. Nothing outside test/ was changed, and I found no defect that needed a failing proof.

New files

• test/invariant/BurnTrackerHandler.sol: a handler that calls the contract in random order with four actors. Before each call it predicts, from the brief's rules (not from the code), whether the call should succeed or revert. It covers:
  • open, updateBurntracker (real proof, another known document, or a one-byte change; maxPrice below, at or above the live price), recover (valid or malformed ids) and setResultHash.
  • Intake results and failures for the awaited order and for orders that were replaced; fake callbacks from other senders.
  • Time moves, donations, withdraw, setTiming (in and out of range), switching setBody between the launch template and another one, and price changes including zero.
  • For each order it checks the exact body bytes the Intake received, that the payer recorded is the contract, and the amount paid.
• test/invariant/BurnTrackerInvariant.t.sol: runs against the deployed BurnTrackerTest with 256 runs × 128 calls, and the handler must never revert. After every call it checks:
  • every call matched the prediction;
  • all status() fields, resultHash and lastRequestId match the model;
  • the contract holds only donations minus withdrawals and leaves no approval to the Intake;
  • every payment reached the treasury, and actor balances add up;
  • the two storage slots a callback writes are never zero;
  • state and kind stay consistent and timing stays in range;
  • the owner never changes.
  • A fixed sequence test shows the handler really reaches every state, both callback types, a malformed but authenticated proof and a replaced order. A probe I ran (not submitted) confirmed random runs do reach real updates and completions.
• test/EdgeCases.t.sol: 12 unit tests and one fuzz test (512 runs) for things the earlier suite didn't pin down:
  • the stale deadline and cooldown checked one second either side;
  • a refused update restarting the cooldown from the moment of refusal;
  • setTiming leaving a placed deadline alone but changing the cooldown;
  • maxPrice one wei below or at the price, and a price raised after it was quoted;
  • every malformed shape of job id rejected;
  • owner-only paths in every state where they're allowed;
  • late callbacks for replaced or manually adopted orders refused;
  • the old owner losing all powers after a handover.
  • The fuzz test checks that an update never charges more than maxPrice or before the cooldown, and leaves no balance or approval behind.

Findings (.imd-findings.json, both info level, no proof needed):

1. A pending ownership nomination can't be cancelled, because transferOwnership(address(0)) reverts; it can only be replaced with another address.
2. A callback the contract rejects (a zero result hash, or a failure status other than 1 or 2) is lost for good. The order then stays pending until its stale time (48 hours here), after which the owner has to recover and pay again. The README documents this, and the real Intake doesn't send these values.

Choices I made where the brief was silent:

• I measured the deadlines as "at or after" the stated time, which is how the contract behaves.
• I treated a duplicate jobId inside a nested object as a second key, so such a document is rejected.

The new files are not committed.