# Aztec Experiments > Source: > Published: 2026-07-20 16:47:19+00:00 An anonymous billboard on Aztec v5 mainnet. Users deposit ETH on L1, post messages anonymously on L2, and withdraw their ETH back to L1. Posts are fully anonymous — no sender address appears in public call data, and there is no link to the L1 deposit. Features: **Censorship mechanism**: A censor (set at deploy time) can flag posts as "immoral". Flagged posts are hidden from the default feed and impose a time-lock penalty on the poster's next post. The censor can transfer rights to another address.**Automated censorship bot**: A local-LLM daemon (`censor-daemon/` ) watches the billboard, evaluates posts against the on-chain moderation policy, and automatically flags violations.**Moderation policy**: The censor can set a text moderation policy on-chain (up to 1488 bytes), shown in the UI and CLI. The daemon reads it as the source of truth.**Partial formal verification**: Security properties (rate limits, censorship screening, privacy, deposit safety) are formally verified in Lean 4 / Verity — 70 proven theorems, zero`sorry` s. See[fv/](/vbuterin/aztec_experiments/blob/master/fv). ``` L1 (Ethereum) L2 (Aztec) ┌──────────────────┐ ┌──────────────────────┐ │ BillboardPortal │ │ Billboard │ │ │ │ │ │ deposit(ETH) │──msg──▶ │ claim_deposit() │ │ records deposit │ │ consumes L1→L2 msg │ │ sends L1→L2 msg │ │ creates DepositNote │ │ │ │ │ │ withdraw(ETH) │◀──msg── │ post() │ │ consumes Outbox │ │ consumes note │ │ sends ETH │ │ stores message │ │ │ │ creates new note │ │ │ │ │ │ │ │ withdraw() │ │ │ │ consumes note │ │ │ │ sends L2→L1 msg │ └──────────────────┘ └──────────────────────┘ ``` **Deposits**: L1 deposit is public (EOA + amount visible on Ethereum)** Posts**: Fully anonymous — no sender address in public call data, no link to L1 deposit** Withdrawals**: Reveals depositor's L1 address (inherent — ETH must go somewhere)** Anonymity set**: All depositors who haven't withdrawn yet Posts are rate-limited by a time-lock stored in a private note. The cooldown is inversely proportional to the deposit amount: ``` cooldown = base_cooldown * min_deposit / amount ``` For example with `base_cooldown=3600, min_deposit=0.001` : - 0.001 ETH → 3600s cooldown (1 post/hour) - 0.005 ETH → 720s cooldown (5 posts/hour) - 0.01 ETH → 360s cooldown (10 posts/hour) Each `post()` advances `next_allowed_time` by one cooldown (or more if flagged posts are screened). Posting multiple times in quick succession is possible if enough time has elapsed since the last post — the **save-up rule** (`max_save_up` ) allows accumulating up to `max_save_up` posts of credit during dormancy, then spending them in quick succession. The deposit→withdraw loop does not help: re-depositing creates a new note with a fresh claim-time lock, identical to simply waiting. A censor (set at deployment time) can flag posts as "immoral" via `declare_immoral(post_index, response)` . Flagged posts are: **Hidden** from the billboard feed by default (user app shows a "View censored posts" link with confirmation dialog)**Flag-penalized**: when a flagged post is screened during a subsequent`post()` call, the next post's time lock is extended by`cooldown * (K-1)` per flag (K set at deploy time). This is equivalent to making K-1 dummy posts at the same time: screening 1 flagged post costs K total cooldowns (1 base + (K-1) penalty). **Screening** uses constant-cost Merkle proofs instead of chain walking. Each `post()` call screens 0–2 older posts (the "child" and "grandchild" in the post chain) via `assert_note_existed_by` . A post can only be screened after the **censor window** (default 3600s) has passed since it was created — guaranteeing the censor time to flag it first. **Withdrawal** requires all real posts to be screened (`last_screened_index >= last_real_post_index` ). Users make **dummy posts** (which advance screening without storing content) to screen their last real post before withdrawing. If no real posts exist, only the initial claim-time lock must expire. The post chain uses a cryptographic link mechanism: each post stores a `prev_link` field computed as `poseidon2_hash_with_separator([inner_note_hash, link_secret], DOM_SEP__POST_LINK)` , where `link_secret` is derived from the poster's nullifier hiding key. This preserves anonymity — no public link between posts is revealed. The censor can transfer censorship rights to another address via `transfer_censor(new_address)` . The deployer has no post-deployment control over the censor. The censor can set a text moderation policy on-chain via `set_moderation_policy(fields, len)` (up to 1488 bytes, stored as 48 Field values). The policy is readable via `get_moderation_policy()` and is displayed in the user app, censor app, and CLI output. The automated censor daemon reads the on-chain policy as the source of truth for moderation decisions. See [SECURITY_PROPERTIES.md](/vbuterin/aztec_experiments/blob/master/SECURITY_PROPERTIES.md) for the full security analysis with line-by-line code references. The `censor-daemon/` directory contains a self-contained daemon that watches the Billboard contract for new posts, runs them through a local LLM (llama.cpp), and automatically flags any that violate the on-chain moderation policy. ``` ┌─────────────┐ ┌──────────────┐ ┌─────────────────┐ │ daemon.mjs │────▶│ llama-server │────▶│ Local LLM │ │ (orchestr) │ │ (port 5090) │ │ (Qwen3.5-2B) │ └──────┬──────┘ └──────────────┘ └─────────────────┘ │ │ subprocess (black-box) ▼ ┌─────────────────────────────┐ │ cli.mjs list --json │ → posts[], censorWindow, policy │ cli.mjs declare-immoral │ → flags post on-chain └─────────────────────────────┘ ``` From any state, running `node daemon.mjs` will: **Download + compile llama.cpp**(if not already present)** Download the model**(~1.4 GB Q4_K_M GGUF, Qwen3.5-2B by default)** Start llama-server**— local OpenAI-compatible API on`127.0.0.1:5090` **Read contract config**— fetches the on-chain moderation policy, censor window, and max save-up** Poll the billboard**— shells out to`cli.mjs list --json` to read all posts**Moderate each post**— sends the post + policy to the LLM, asks "VIOLATION or OK?"** Flag violations**— shells out to`cli.mjs declare-immoral` to flag the post on-chain The daemon is a **thin orchestrator** — it never touches the Aztec SDK directly. All on-chain operations go through the existing user CLI as black-box subprocess calls. It is **censor-window-aware**: it prioritizes posts closest to expiring (oldest first), warns on posts with <5 minutes left, and warns on posts already past the censor window. Policy resolution order: on-chain policy (from `get_moderation_policy()` ) → local `policy.txt` → hardcoded default. ``` # Dry-run (evaluate but don't flag on-chain): node censor-daemon/daemon.mjs --dry-run --once # Live (actually flag violations): node censor-daemon/daemon.mjs --poll-interval 30 ``` Tests: 23 unit tests (`test_moderation.mjs` ) + 14 integration tests (`test_daemon.mjs` ) with mock infrastructure — no network or llama.cpp required. Run `bash censor-daemon/run_tests.sh` . See [censor-daemon/README.md](/vbuterin/aztec_experiments/blob/master/censor-daemon/README.md) for full details. Before interacting with L2, you need Fee Juice to pay transaction fees. This app handles the full flow: **Swap ETH→AZTEC**(optional) — If you don't already have AZTEC tokens, the app swaps ETH for AZTEC via Uniswap V3 on L1.** Deposit to L2**— Approves the FeeJuicePortal and deposits AZTEC tokens, sending an L1→L2 message.** Scan / Recover**— Scans L1`DepositToAztecPublic` events backwards to find your deposit, derives the claim secret from your ETH wallet signature, and checks nullifier consumption + checkpoint status.**Claim on L2**— Consumes the L1→L2 message to mint Fee Juice on L2. Also supports an `auto` action that runs deposit → wait → claim in one go. Deploys and links the billboard contracts. The deployment has a circular dependency (L1 portal needs L2 address, L2 contract needs L1 portal address), broken by making the L2 constructor take no arguments and setting the portal later. **Deploy L2**— Deploys the Noir Billboard contract using universal deploy (address depends only on salt + artifact, not deployer wallet).**Deploy L1 Portal**— Deploys the Solidity portal via CREATE2 (deterministic from L2 address + rollup + version).** Link Portal**— Calls`update_portal()` on L2 to store the L1 portal address.**Cross-Check**— Verifies L1→L2 and L2→L1 references match. The main user-facing app. Full flow: deposit → claim → post → withdraw → claim on L1. **Deposit ETH**— Deposits ETH into the L1 portal (sends an L1→L2 message).** Claim on L2**— Consumes the L1→L2 message to create a private DepositNote.** Post**— Posts an anonymous message. Each post extends the time lock by one cooldown. The billboard feed auto-refreshes every 5 seconds.**Withdraw**— Consumes the DepositNote and sends an L2→L1 message.** Claim on L1**— After the epoch proof (~40 min on mainnet), consumes the Outbox message to claim ETH on L1. The billboard feed **hides censored posts by default**. A "View censored posts" link at the bottom shows how many posts are hidden; clicking it opens a confirmation dialog ("These posts have been flagged as immoral by the censor. Are you sure you want to see them?"). Confirming reveals the censored posts with grey styling and a "Hide censored posts" toggle to hide them again. The `auto` action runs the full flow end-to-end autonomously. A dedicated app for the censor to manage censorship. No ETH wallet needed — the censor only operates on L2. **Load censor wallet**— Load the censor's Aztec wallet (the one whose address was passed to`init` at deploy time, or the one that received rights via`transfer_censor` ).**Flag posts**— Enter a post index and optional response text, then flag it as immoral. Flagged posts are hidden from the user billboard by default. When a flagged post is later screened during a subsequent post, the poster's next post time lock is extended by (K-1) extra cooldowns per flag.**Transfer rights**— Transfer censorship authority to another Aztec address.** View billboard**— The censor sees all posts including flagged ones (with censor response messages). The censor is set at `init()` time only — the deployer cannot change it after deployment. Only the censor can transfer rights to another address. ``` aztec/ ├── README.md ← this file ├── SECURITY_PROPERTIES.md ← security analysis with code references ├── wallet.json ← Aztec wallet (secret key + salt) ├── eth_wallet.json ← ETH wallet (private key) ├── package.json ← ethers + fake-indexeddb (for CLIs) │ ├── billboard/ ← Contracts │ ├── Nargo.toml ← Noir workspace │ ├── billboard_contract/ ← L2 contract (Noir) │ │ ├── Nargo.toml │ │ └── src/ │ │ ├── main.nr ← Billboard contract │ │ └── lib.nr ← Helpers: msg hashes, cooldown computation │ ├── portal/ ← L1 contract (Solidity / Foundry) │ │ ├── foundry.toml │ │ └── src/ │ │ └── BillboardPortal.sol │ └── target/ ← Compiled Noir artifacts (gitignored) │ ├── shared/ ← Shared modules (used by all apps) │ ├── styles.css ← Dark theme CSS │ ├── helpers.js ← UI helpers: logging, pagination, extractors │ ├── wallet-buttons.js ← Common wallet loading/generation UI module │ ├── app-env.js ← Common browser env builders (buildEnv, buildConfig, makeCallEngine) │ ├── aztec-lib.js ← PXE/CRS/wallet infrastructure + Fee Juice constants │ ├── aztec_bundle.js ← Aztec PXE bundle (WASM, ~58MB) │ ├── ethers.min.js ← ethers v6 (for L1 interactions) │ ├── poseidon2.js ← Pure-JS Poseidon2 (verified against bb.js) │ └── rpc-config.json ← Aztec node URL + API key │ ├── apps/ ← Web apps + CLIs │ ├── build.mjs ← Build script (combines modules → single-file HTML) │ ├── serve.py ← Dev server with COOP/COEP headers for multi-threaded WASM │ ├── src/ │ │ ├── fee-juice/ ← Fee Juice app │ │ │ ├── template.html │ │ │ ├── app.js ← Thin wrapper (UI → engine) │ │ │ ├── engine.js ← Fee Juice flow logic (swap, deposit, scan, claim) │ │ │ ├── cli.mjs ← CLI tool (same engine, Node.js) │ │ │ └── pxe-cache.cjs ← IndexedDB dump/restore for CLI PXE caching │ │ └── billboard/ │ │ ├── billboard_artifact.json ← Compiled L2 contract artifact │ │ ├── portal_bytecode.txt ← Compiled L1 portal bytecode │ │ ├── build_artifact.mjs ← Artifact build script (VKs, bytecode) │ │ ├── build_vks.sh ← VK computation helper │ │ ├── deploy/ ← Deploy app │ │ │ ├── template.html │ │ │ ├── app.js ← Thin wrapper │ │ │ ├── engine.js ← Deploy flow (L2 + L1 + link + cross-check) │ │ │ ├── cli.mjs ← CLI tool │ │ │ ├── gen_eth_wallet.mjs ← ETH wallet generator │ │ │ ├── gen_censor_wallet.mjs← Censor Aztec+ETH wallet generator │ │ │ ├── gen_user_wallet.mjs ← User Aztec+ETH wallet generator │ │ │ ├── billboard_artifact.json │ │ │ └── portal_bytecode.txt │ │ ├── censor/ ← Censor app │ │ │ ├── template.html │ │ │ ├── app.js ← Flag posts, transfer rights, view all posts │ │ │ ├── engine.js ← Symlink → user/engine.js (shared engine) │ │ │ └── pxe-cache.cjs ← Symlink → user/pxe-cache.cjs │ │ └── user/ ← User app │ │ ├── template.html │ │ ├── app.js ← Thin wrapper (UI → engine, live feed, censored post hiding) │ │ ├── engine.js ← User flow (deposit, claim, post, withdraw, claim-l1, declare-immoral, transfer-censor) │ │ ├── cli.mjs ← CLI tool │ │ └── pxe-cache.cjs ← IndexedDB dump/restore for CLI PXE caching │ ├── dist/ ← Built single-file apps │ │ ├── fee-juice.html │ │ ├── deploy.html │ │ ├── user.html │ │ ├── censor.html │ │ ├── aztec_bundle.js ← Copy of the PXE bundle │ │ └── crs/ ← CRS files for proving │ ├── censor-daemon/ ← Automated censorship bot (local LLM) │ ├── daemon.mjs ← Orchestrator: llama.cpp setup, polling, flagging │ ├── moderation.mjs ← LLM moderation logic (prompt, verdict parsing) │ ├── policy.txt ← Default moderation policy (fallback) │ ├── test_moderation.mjs ← Unit tests for moderation parsing (23 tests) │ ├── test_daemon.mjs ← Integration tests with mock infra (14 tests) │ ├── run_tests.sh ← Test runner script │ └── README.md ← Full daemon documentation │ ├── fv/ ← Formal verification (Lean 4 + Verity) │ ├── PLAN.md ← Verification plan and status │ ├── billboard_aztec_lean/ ← Lean model of L2 Noir contract (51 theorems) │ │ └── BillboardAztec.lean │ ├── billboard_portal_verity/ ← Verity port of L1 Solidity portal (12 theorems) │ │ ├── BillboardPortal.lean │ │ ├── Spec.lean, Invariants.lean │ │ └── Proofs/Basic.lean │ ├── bridge_model/ ← Lean model of L1↔L2 bridge (7 theorems) │ │ └── Bridge.lean │ └── notes/ │ └── SECURITY_PROPERTIES_FORMAL.md ← Theorem-by-theorem mapping (P1-P18, I1-I12) │ ├── .pxe-cache/ ← CLI PXE cache (IndexedDB dumps, gitignored) │ └── node_modules/ ← ethers, fake-indexeddb ``` Each app follows the same pattern: — All business logic. Takes an`engine.js` `env` object (`{ aztec, ethers, log, initCRS, createStore, getEthSigner, portalBytecode, artifact }` ) and a`config` object. Returns`{ ok, state, handles }` where`handles` gives the web UI access to live PXE/contract objects for polling.— Thin UI wrapper. Builds`app.js` `env` /`config` from UI state, calls the engine with the appropriate action, routes`log` callbacks to page-specific status divs.— CLI tool. Same engine, Node.js environment. Polyfills IndexedDB with`cli.mjs` `fake-indexeddb` , loads the bundle, runs the engine. Both the web UI and CLI share the same engine, so any flow that is autonomous in the CLI is also autonomous in the web UI. **Fee Juice**: `status` , `scan` , `deposit` , `claim` , `auto` **User**: `status` , `deposit` , `claim` , `post` , `list` , `withdraw` , `claim-l1` , `declare-immoral` , `transfer-censor` , `auto` **Deploy**: `status` , `deploy` The `auto` action runs the full flow end-to-end: deposit → wait for L2 ingest → claim → post (if message provided) → withdraw → claim-l1. **Censor daemon**: `daemon.mjs` is not an engine action but a standalone orchestrator that shells out to `cli.mjs list --json` and `cli.mjs declare-immoral` as subprocesses. See [censor-daemon/README.md](/vbuterin/aztec_experiments/blob/master/censor-daemon/README.md). ``` # 1. Compile L2 contract (aztec compile transpiles public ACIR → AVM bytecode + adds VKs) cd billboard && aztec compile # 2. Build the artifact (computes VKs with chonkComputeVk, packages bytecode) cd apps/src/billboard && node build_artifact.mjs cp billboard_artifact.json deploy/billboard_artifact.json # 3. Compile L1 portal (if portal_bytecode.txt needs updating) cd billboard/portal && forge build --use 0.8.33 # 4. Build all dapps (combines modules into single-file HTML) cd apps && node build.mjs cd fv/verity export PATH="$HOME/.elan/bin:$PATH" lake build # 2125 jobs, zero sorrys ``` The L2 contract's `Nargo.toml` must depend on `aztec-nr` tag `v5.0.0` — the same version the `aztec_bundle.js` was built from. Version mismatches cause standard contract addresses (HandshakeRegistry, AuthRegistry, etc.) baked into the ACIR to differ from those registered in PXE, causing "contract is not registered" errors. Each recompilation changes the contract class ID (public bytecode commitment), so always use a salt that was never used before when deploying. ``` # Fee Juice (swap ETH→AZTEC, deposit, claim — all in one) node apps/src/fee-juice/cli.mjs --gen-all # Generate new wallets node apps/src/fee-juice/cli.mjs --status --aztec-wallet wallet.json --eth-wallet eth_wallet.json node apps/src/fee-juice/cli.mjs --scan --aztec-wallet wallet.json --eth-wallet eth_wallet.json node apps/src/fee-juice/cli.mjs --eth-for-swap 0.005 --aztec-wallet wallet.json --eth-wallet eth_wallet.json # Billboard user (deposit → claim → post → withdraw → claim-l1) node apps/src/billboard/user/cli.mjs status --contract-salt 2028 --aztec-wallet wallets/user_aztec_wallet.json --eth-wallet wallets/user_eth_wallet.json node apps/src/billboard/user/cli.mjs deposit --contract-salt 2028 --amount 0.002 --aztec-wallet wallets/user_aztec_wallet.json --eth-wallet wallets/user_eth_wallet.json node apps/src/billboard/user/cli.mjs post --contract-salt 2028 --msg "hello world" --aztec-wallet wallets/user_aztec_wallet.json --eth-wallet wallets/user_eth_wallet.json \ --censor 0x0035abfebdafd10697b8a9a5de2792715602ff077787ca6cfefdab632547189f --k-multiplier 4 node apps/src/billboard/user/cli.mjs list --contract-salt 2028 --aztec-wallet wallets/user_aztec_wallet.json --eth-wallet wallets/user_eth_wallet.json \ --censor 0x0035abfebdafd10697b8a9a5de2792715602ff077787ca6cfefdab632547189f --k-multiplier 4 node apps/src/billboard/user/cli.mjs withdraw --contract-salt 2028 --aztec-wallet wallets/user_aztec_wallet.json --eth-wallet wallets/user_eth_wallet.json \ --censor 0x0035abfebdafd10697b8a9a5de2792715602ff077787ca6cfefdab632547189f --k-multiplier 4 # Censor: flag posts and transfer rights node apps/src/billboard/user/cli.mjs declare-immoral --contract-salt 2028 --post-index 0 --censor-response "spam" \ --censor 0x0035abfebdafd10697b8a9a5de2792715602ff077787ca6cfefdab632547189f --k-multiplier 4 \ --censor-wallet wallets/censor_aztec_wallet.json node apps/src/billboard/user/cli.mjs transfer-censor --contract-salt 2028 --new-censor 0x... \ --censor 0x0035abfebdafd10697b8a9a5de2792715602ff077787ca6cfefdab632547189f --k-multiplier 4 \ --censor-wallet wallets/censor_aztec_wallet.json python3 apps/serve.py [port] # default: 5000 (project convention) ``` Sets COOP/COEP headers for `SharedArrayBuffer` (multi-threaded WASM) and serves from `apps/dist/` . Local CRS files in `apps/dist/crs/` are loaded automatically. The L2 contract is deployed with `universalDeploy: true` and `publicKeys: deriveKeys(Fr.ZERO).publicKeys` , so the contract address depends only on the salt + artifact — not the deployer's wallet. This means the deploy and user apps always compute the same address. The v5 bundle uses the initializerless Schnorr account contract for self-deployment. The regular SchnorrAccountContract stores its signing key in a private note created by the constructor, but during self-deployment (deploy + claim fee juice in one tx), the entrypoint runs before the constructor, so `get_note()` fails. The initializerless variant stores the signing key in a PXE capsule and verifies against `immutables_hash` . The web apps run the full PXE stack entirely in the browser: **IndexedDB store** for PXE state (data directory includes wallet address for isolation)**CRS files** loaded from local files first, falling back to CDN**Proving** via`bb.js` WASM (multi-threaded when COOP/COEP headers are set)**No backend server**— all RPC goes directly to the Aztec node Both CLIs dump/restore the in-memory IndexedDB state to `~/.pxe-cache/` between runs, saving ~2-4s on PXE sync. Cache files are keyed by account address. The shared `wallet-buttons.js` module provides a common wallet UI across all three apps with: **ETH wallet**: Load from JSON, Generate random, or connect browser wallet** Aztec wallet**: Load from JSON, Generate random, or derive from ETH wallet (sign a message, use signature as secret key)- Color-coded button states and auto-advancement when all wallets are loaded **nargo**/** aztec**CLI (must match the v5 bundle version)** forge**(Foundry, for compiling the Solidity portal)** Node.js**≥ 24- A browser wallet for L1 transactions (in the web UI) **Lean 4 / elan**(only for building formal verification proofs in`fv/` ) The `fv/` directory contains a partial formal verification of the billboard's security properties using [Verity](https://veritylang.com) (Lean 4 framework for verified smart contracts) and a standalone Lean model of the L2 contract. **Build status: 2125 Lean jobs, zero sorrys, 70 proven theorems/lemmas.** | Component | File | Theorems | Axioms | Status | |---|---|---|---|---| L2 model (Lean) | `fv/billboard_aztec_lean/BillboardAztec.lean` | 51 | 5 | Constant-cost screening model: I1–I12, deposit safety, privacy | L1 portal (Verity) | `fv/billboard_portal_verity/` | 12 | 1 | Solidity port rewritten as `verity_contract` , guard proofs + conservation | Bridge model (Lean) | `fv/bridge_model/Bridge.lean` | 7 | 2 | Inbox/Outbox no-double-consume, content-hash agreement | **L2 model** (51 theorems, models the Noir contract's constant-cost screening design from [LATEST_CHANGE.md](/vbuterin/aztec_experiments/blob/master/LATEST_CHANGE.md)): **I1**— Constant-cost screening: each`post()` screens at most 2 posts (zero axioms)**I3**— Censor window guarantee: posts only screened after`censor_window` expires (zero axioms)**I4**— Monotonic advance:`last_screened` never goes backwards (zero axioms)**I5**— Flag penalty: each flag adds exactly`cooldown × (K-1)` (zero axioms)**I6**— Save-up rule bounds burst posting (zero axioms)** I7**— Withdrawal requires full screening (zero axioms)** I10**— Chain link unforgeability (uses`poseidon2_injective` axiom)**Master safety theorem**(`deposit_safety_master` ): withdraw ≤`T_stop + ⌈N/2⌉ × C × (1+(K-1)×2)` — no permanent lockout**Master privacy theorem**(`post_unlinkability_master` ): two posts by same user are indistinguishable from two by different users (constructive proof, zero axioms)**Censor governance**: only censor can flag/transfer/set-policy (proven) **L1 portal** (7 Verity proofs + 5 stubs): P2 (no double deposit), P3 (withdraw zeroes balance), P4 (no withdraw without deposit), P14 (u128 overflow), conservation of `totalDeposited` . **Bridge**: no-double-consume for Inbox and Outbox, content-hash agreement axioms (P1/P16). 8 axioms total, all at cryptographic/platform trust boundaries: `poseidon2_injective` — hash injectivity (cryptographic assumption)`nhk_app_opacity` — link_secret not derivable from public data (cryptographic)`nullifier_unlinkability` — nullifiers don't reveal owner (Aztec platform property)`deposit/withdraw_hash_agreement` — L1 and L2 agree on content hashes (bridge boundary)`externalCallStubBool_true` — Verity test stub for external calls returns`true` See [fv/notes/SECURITY_PROPERTIES_FORMAL.md](/vbuterin/aztec_experiments/blob/master/fv/notes/SECURITY_PROPERTIES_FORMAL.md) for the full theorem-by-theorem mapping, and [fv/PLAN.md](/vbuterin/aztec_experiments/blob/master/fv/PLAN.md) for the verification plan. - **Strengthen end-to-end FV theorems**— The bridge soundness theorems (P1, P5, P16) and several L2 invariants (I2, I8, I9, I11, I12) are currently stated as`True := by trivial` . Strengthen these to full proofs connecting L1 Verity + L2 Lean + bridge model. - **Replace in-app JSON Ethereum wallet with**— The current "Load from JSON" ETH wallet option requires users to manually export and load a private key JSON file. Replace this with OpenLV integration for a more secure, user-friendly wallet connection.[OpenLV](http://openlv.sh/) - **End-to-end browser test of censor app**— The censor web app (`censor.html` ) has been built but not yet tested in a browser. The CLI`declare-immoral` and`transfer-censor` actions have been fully tested on mainnet (salt 2028). - **End-to-end browser test of censored post hiding**— The "View censored posts" confirmation dialog and grey styling have been implemented in the user app but not yet tested in a browser against live mainnet data. - **Add access control guard to**— Currently anyone can call it first with a bogus address, bricking the contract (griefing DoS, not theft). Should be deployer-only or called in the same L2 tx batch as deploy. See`update_portal()` [SECURITY_PROPERTIES.md](/vbuterin/aztec_experiments/blob/master/SECURITY_PROPERTIES.md)§5. - **Fix**— Theoretically wraps after ~134M posts, overwriting post 0. Economically unreachable today but should be fixed for correctness.`post_count` /`post_data` key type from u32 to u64/Field - **Fix**— Over-counts across deposit/withdraw cycles (never decremented). Not security-relevant (withdrawals read`totalDeposited` accounting drift`deposits[msg.sender]` , not the total) but cosmetically wrong. - **Surface L1 withdrawal claim in the web UI**— The`claim-l1` action exists in the engine/CLI but the web UI doesn't expose it as a distinct page with Outbox proof input. - **Add "view on explorer" links** for confirmed L2 transactions (e.g. aztecscan.com). - **Show estimated wait time** for epoch proofs in the UI during claim-l1 (~40 min on mainnet). - **Suppress verbose PXE/bundle console output** in the browser — Partially done, but pino logger output still leaks through to the console. - **Add transient RPC retry logic to web apps**— The CLI has this via a`TRANSIENT_RE` regex; the web apps may not. - **Handle multiple deposits to different Aztec addresses from the same ETH wallet**— Fee-juice scan filters by`to` address, but the UX could be clearer about which deposit is being claimed. - **Withdraw deposits on old test deployments**— Salts 2025, 2026, 2027, 2028 have deposits that can be withdrawn to recover ETH.