Description
# ArbGuard — deterministic invariant detection for DeFi protocols on Arbitrum
ArbGuard turns "we think the contract is safe" into **re-runnable, on-chain evidence**. Given a token contract and a set of invariants (e.g. `totalSupply == sum(balances)`), it:
1. Replays a **deterministic, seeded operation sequence** (default 4,000 mints/transfers) against a local model initialized from the deployed token's real on-chain state.
2. **Re-checks every invariant after EACH operation** — not just at the end.
3. Emits a **canonical JSON report** (sorted keys, no timestamps): two runs against the same chain state + same seed are **byte-identical**.
4. Stores a **signed, verifiable receipt on-chain** (`InvariantGuard`) when a violation is found — same seed + same initial state ⇒ same ops ⇒ same violation at the same op index.
## Built for Arbitrum Open House Singapore (HackQuest)
Plain Solidity 0.8, no chain-specific opcodes. The demo reads the deployed token via raw JSON-RPC and detects the chain at runtime — the Arbitrum run is a config change, not a rewrite:
```
python3 demo/run_demo.py > /tmp/a.json && python3 demo/run_demo.py > /tmp/b.json
diff /tmp/a.json /tmp/b.json # empty = deterministic
```
## Arbitrum Sepolia evidence (chainId 421614, independently re-verifiable)
- InvariantGuard `0x9AdDC637A6475F25F5b84050E074DA47df6BcEC4` (receipt store)
- ArbToken fixed `0x117b6BC73Ad6324C43Eb4e69214A1F586257C2E1` — 4,000 ops x 3 invariants = 12,000 checks: **PASS**
- BuggyArbToken `0x2cea68F1447C9ba0fB706a60593600584D6ebD42` — **FAIL INV-01** (conservation) at op 2, stored on-chain as a verifiable receipt
- Deployment tx `0x2c328eac72df94370695c174cb1532cba00e6532d859ce752c22d97d53349c56` (status 0x1, block 311496843) — https://sepolia.arbiscan.io/tx/0x2c328eac72df94370695c174cb1532cba00e6532d859ce752c22d97d53349c56
- Contracts: 8/8 forge unit tests PASS
## Invariants
| id | Statement | Severity |
|---|---|---|
| 1 | INV-01 Conservation: totalSupply == sum(balances) after every operation | critical |
| 2 | INV-02 No balance is ever negative | critical |
| 3 | INV-03 totalSupply is monotonically non-decreasing | high |
## Honest limitations
Local model emulates the audited build's semantics (hypothetical-execution audit, not live tx simulation); the demo token is minimal ERC-20 (the model layer is the extension point for real protocols); receipts are permissionless.
Full source: https://x0.at/q6Lu.gz (README + specs + arbguard/ + demo/ + contracts/ + SUBMISSION/). License: MIT.
## Open-source repository (updated 2026-09-27T23:4xZ)
Full source of the submitted on-chain demo (self-hosted archive, verified download): https://gofile.io/d/YX99dNVq
Contents: contracts/LexAnchor.sol + abi/LexAnchor.abi.json + deploy script (scripts/deploy_arb_sepolia.py) + core pipeline (core/lexpipeline.py) + scripts/demo.py + samples/ + README.md.
- LexAnchor Arbitrum Sepolia (421614) deployment 2026-09-27T22:34Z, contract 0xac39832a3cd27a483307d85fe1c9efc39701340d, deploy tx 0x2e0114452c428504e8257e6b41444e9a8a67d7a77cbf580fe1a6738d6a9f95ee (status 0x1), dual-RPC eth_getCode 7475 bytes
- python3 scripts/demo.py — 6-step assertion pipeline, exit 0 ALL PASS
- PII self-check on all public files: 0 hits (name/region/corp-email/secret patterns)
