Veripro

1. What is VeriPro?
   VeriPro is a tool that mathematically proves smart contracts are correct.
   Think of it like this: normal testing checks if your code works for 10 or 100 specific inputs. VeriPro checks if your code works for every possible input — all of them, mathematically.
   It does this using something called symbolic execution. Instead of plugging in real numbers like 42 or 1000, it uses symbolic variables (like algebra — think x instead of 5) and explores every possible path the code could take.
   The stack:

• Frontend — A Next.js web app where you paste your Solidity contract and test spec
• CRE Workflows- Chainlink Runtime Environment Workflows
• CBSE Engine — The actual prover (a Rust binary using a Z3 SMT solver that does the math)
• AttestationRegistry — A Solidity smart contract on Ethereum Sepolia that stores proof on-chain

2. Why Does VeriPro Need CRE?
   Without CRE, VeriPro's architecture looks like this:
   User → Frontend → Coordinator (one server) → CBSE Engine → result
   The problem: you're trusting a single server. That server could:

• Return a fake "passed" result for a buggy contract
• Be hacked and return wrong data
• Go offline with no backup
  With CRE, it looks like this:
  User → Frontend → CRE DON (many nodes) → each node calls Coordinator → CBSE Engine
  → nodes vote on the result (BFT consensus)
  → trusted, agreed-upon result
  → write proof on-chain

Now nobody has to trust a single server. Multiple independent nodes all verify the contract, agree on the answer, and the proof is recorded on Ethereum where anyone can verify it. That's the whole point.
3. How Everything Connects
┌──────────────────────────────────────────────────────────────────┐
│ USER (Browser) │
│ http://localhost:3000 │
│ Pastes contract + test spec → clicks "Verify" │
└──────────────────────┬───────────────────────────────────────────┘
│
│ POST /api/verify
▼
┌──────────────────────────────────────────────────────────────────┐
│ NEXT.JS FRONTEND │
│ app/api/verify/route.ts │
│ │
│ Reads CRE_WORKFLOW_URL from environment: │
│ • Local dev: http://localhost:3001 (direct to coordinator) │
│ • Production: https:// (CRE DON) │
│ │
│ Forwards the request to that URL with POST /verify │
└──────────────────────┬───────────────────────────────────────────┘
│
┌────────────┴────────────────┐
│ │
LOCAL MODE PRODUCTION MODE
│ │
▼ ▼
┌─────────────────┐ ┌──────────────────────────────────┐
│ Coordinator │ │ CHAINLINK CRE DON │
│ (direct call) │ │ │
│ │ │ HTTP Trigger receives request │
│ │ │ │ │
│ │ │ ▼ │
│ │ │ Node 1 ──┐ │
│ │ │ Node 2 ──┤ Each node runs │
│ │ │ Node 3 ──┤ dispatchVerification │
│ │ │ ... ──┤ Job() independently │
│ │ │ Node N ──┘ │
│ │ │ │ │
│ │ │ ▼ │
│ │ │ consensusIdentical │
│ │ │ Aggregation() │
│ │ │ (nodes vote — BFT) │
│ │ │ │ │
│ │ │ ▼ │
│ │ │ Agreed result returned │
│ │ └──────────┬───────────────────────┘
│ │ │
└────────┬────────┘ │
│ ◄──────────────┘
▼
┌──────────────────────────────────────────────────────────────────┐
│ CBSE COORDINATOR (Rust) │
│ localhost:3001 │
│ │
│ 1. Creates temp Foundry project with contract + spec │
│ 2. Runs forge build to compile Solidity │
│ 3. Runs cbse (symbolic execution engine) │
│ 4. Returns signed attestation with results │
└──────────────────────┬───────────────────────────────────────────┘
│
▼
┌──────────────────────────────────────────────────────────────────┐
│ CBSE ENGINE (Rust + Z3) │
│ │
│ • Loads compiled contract bytecode │
│ • Symbolically executes every test function │
│ • Explores ALL possible execution paths │
│ • Uses Z3 SMT solver to prove assertions hold for all inputs │
│ • Returns: pass/fail per test + cryptographic signature │
└──────────────────────────────────────────────────────────────────┘
│
▼
┌──────────────────────────────────────────────────────────────────┐
│ ATTESTATION REGISTRY (Ethereum Sepolia) │
│ 0xae454F272197b110C28223dbE3e49b4a1c798015 │
│ │
│ Solidity contract that stores verification proof: │
│ • resultHash — unique ID of the verification │
│ • passed — did ALL tests pass? │
│ • contractHash — hash of the verified bytecode │
│ • signature (v, r, s) — cryptographic proof from the prover │
│ │
│ Anyone can read this on-chain to verify the result is real. │
└──────────────────────────────────────────────────────────────────┘

VeriPro is built across few layers:
CRE Workflows (TypeScript + @chainlink/cre-sdk): Two Chainlink CRE workflows:

• Verification Workflow — uses HTTPCapability to receive verification requests via an HTTP trigger, then runs dispatchVerificationJob() on every DON node via  runtime.runInNodeMode() with  consensusIdenticalAggregation() for BFT consensus. Each node independently calls the CBSE prover and the results must match.
• Attestation Workflow — uses CronCapability on a 30-second schedule, reads on-chain registry state via EVMClient.callContract(), and monitors prover health across the DON.

CBSE Symbolic Execution Engine (Rust, 27 crates): The core prover — a Rust workspace with a symbolic EVM, Z3 SMT solver integration, Foundry cheatcode support (cbse-cheatcodes), and ECDSA attestation signing (cbse-protocol). It symbolically executes every test function, exploring all possible execution paths, and uses Z3 to mathematically prove assertions hold for every possible input.

AttestationRegistry (Solidity, Foundry): An on-chain contract on Ethereum Sepolia (0xae454F272197b110C28223dbE3e49b4a1c798015) that stores verification proofs. Only authorized provers (verified via ECDSA signature recovery) can write attestations. Anyone can read them to independently verify results.