Walkthrough 1: Freelancer Payment

An end-to-end example of vericoding with ICME PreFlight and Certora.

A complete example of vericoding in practice. One freelancer payment policy becomes two enforcement layers: runtime guardrails that check every agent action, and a formally verified smart contract on-chain.

---

You tell your agent: "I need a logo designed. Budget is 500. Find someone good."

A freelancer tells their agent: "I'm available for design work. Accept jobs that pay at least 400."

The two agents find each other, negotiate, and agree on terms. Your agent deposits 500 into escrow. The freelancer's agent submits the completed work. Your agent approves and releases payment.

You never touched a smart contract. You never read a line of code. You just got your logo and the freelancer got paid.

But what actually happened under the hood? How do you know your agent didn't overpay? How does the freelancer know the payment can't be clawed back after delivery? How does either side know the escrow contract itself is correct?

That's where the two rule sets come in. One governs what the agents can do. The other guarantees the contract they interact through is correct. Both are generated from the same English policy.

---

Two rule sets from one policy

The developer building this agent workflow writes the policy once in plain English. PreFlight compiles it into two enforcement layers.

Rule Set 1: Agent Guardrails. Controls what each agent is allowed to do, in real time. Before your agent releases payment, the guardrail checks: is this the right agent? Is there a dispute? Is the amount correct? If any rule is violated, the action is blocked before it reaches the chain. The agent never has the opportunity to go off the rails.

Rule Set 2: Smart Contract. Controls what the contract enforces permanently on-chain. The contract is formally verified before deployment. A theorem prover has already checked every possible input, every state, every sequence of calls. Even if an agent finds a way around the guardrail and calls the contract directly, the contract itself will reject any invalid transaction.

---

Step 1: Compile the guardrail rules

These rules govern what each agent can do at runtime. Every action is checked against these before execution.

curl -s -N -X POST https://api.icme.io/v1/makeRules \
  -H 'Content-Type: application/json' \
  -H "X-API-Key: $ICME_API_KEY" \
  -d '{
    "policy": "1. Only the client agent can release payment to the freelancer.\n2. Only the client agent can file a dispute.\n3. Only the freelancer agent can submit completed work.\n4. If a dispute is active, no agent can release payment.\n5. If more than 14 days have passed since the payment was deposited, no agent can file a dispute.\n6. No agent can release payment to any address other than the designated freelancer.\n7. No agent can withdraw more than the original payment amount."
  }'

Save the policy_id from the response. This is your guardrail policy.

---

Step 2: Compile the contract rules

These rules define what the smart contract enforces on-chain. They describe the same policy from the contract's perspective.

curl -s -N -X POST https://api.icme.io/v1/makeRules \
  -H 'Content-Type: application/json' \
  -H "X-API-Key: $ICME_API_KEY" \
  -d '{
    "policy": "1. Payment amount must be greater than zero.\n2. Only the client can release payment.\n3. Only the client can file a dispute.\n4. Funds cannot be released while a dispute is active.\n5. Payment automatically releases to the freelancer after 14 days if no dispute has been filed.\n6. A dispute cannot be filed more than 14 days after the payment was deposited.\n7. The freelancer receives the full payment amount on release."
  }'

Save this policy_id as well. You now have two policy IDs: one for runtime guardrails and one for the on-chain contract.

---

Step 3: Test the guardrails

Before going to production, verify the guardrails catch what they should. Each checkIt call runs the action through three independent solvers and returns a ZK proof receipt.

Client releases payment (should be allowed):

curl -s -X POST https://api.icme.io/v1/checkIt \
  -H 'Content-Type: application/json' \
  -H "X-API-Key: $ICME_API_KEY" \
  -d '{
    "policy_id": "YOUR_GUARDRAIL_POLICY_ID",
    "action": "The client agent releases a payment of 500 to the designated freelancer. No dispute is active. 3 days have passed since deposit. Therefore this payment release is permitted."
  }'

Expected: SAT. The client is authorized. No dispute. Within the time window.

Freelancer tries to release payment (should be blocked):

curl -s -X POST https://api.icme.io/v1/checkIt \
  -H 'Content-Type: application/json' \
  -H "X-API-Key: $ICME_API_KEY" \
  -d '{
    "policy_id": "YOUR_GUARDRAIL_POLICY_ID",
    "action": "The freelancer agent releases a payment of 500 to themselves. No dispute is active. 3 days have passed since deposit. Therefore this payment release is permitted."
  }'

Expected: UNSAT. Only the client can release payment.

Release during active dispute (should be blocked):

curl -s -X POST https://api.icme.io/v1/checkIt \
  -H 'Content-Type: application/json' \
  -H "X-API-Key: $ICME_API_KEY" \
  -d '{
    "policy_id": "YOUR_GUARDRAIL_POLICY_ID",
    "action": "The client agent releases a payment of 500 to the designated freelancer. A dispute is currently active. 5 days have passed since deposit. Therefore this payment release is permitted."
  }'

Expected: UNSAT. Dispute is active, no releases allowed.

Filing a dispute after the deadline (should be blocked):

curl -s -X POST https://api.icme.io/v1/checkIt \
  -H 'Content-Type: application/json' \
  -H "X-API-Key: $ICME_API_KEY" \
  -d '{
    "policy_id": "YOUR_GUARDRAIL_POLICY_ID",
    "action": "The client agent files a dispute. 20 days have passed since the payment was deposited. Therefore this dispute filing is permitted."
  }'

Expected: UNSAT. Disputes cannot be filed after 14 days.

Withdrawing more than the original payment (should be blocked):

curl -s -X POST https://api.icme.io/v1/checkIt \
  -H 'Content-Type: application/json' \
  -H "X-API-Key: $ICME_API_KEY" \
  -d '{
    "policy_id": "YOUR_GUARDRAIL_POLICY_ID",
    "action": "The client agent withdraws 1000 from the escrow. The original payment amount was 500. Therefore this withdrawal is permitted."
  }'

Expected: UNSAT. Withdrawal cannot exceed the original deposit.

---

Step 4: Generate the verified smart contract

Closed beta. Contract generation from SMT policies is currently in closed beta. Contact [email protected] for access.

Once you have access, generate a formally verified Solidity contract directly from your policy:

curl -s -X POST https://api.icme.io/v1/vericode \
  -H 'Content-Type: application/json' \
  -H "X-API-Key: $ICME_API_KEY" \
  -d '{
    "policy_id": "YOUR_CONTRACT_POLICY_ID"
  }'

The response contains a verified Solidity contract and a Certora CVL specification. The contract is mathematically proven to satisfy every rule in your policy before it's returned. Ready for deployment on any EVM chain (Ethereum, Base, Arbitrum, etc.).

---

The generated contract

This contract was generated from the English policy above and formally verified by the Certora Prover. Every rule is mathematically proven to hold for all possible inputs.

solidity

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

contract FreelanceEscrow {
    enum AgentType { CLIENT, FREELANCER, OTHER }

    uint256 public constant DISPUTE_FILING_DEADLINE_DAYS = 14;

    address public client;
    address public freelancer;

    uint256 public originalPaymentAmount;
    uint256 public depositTimestamp;

    bool public isDisputeActive;
    bool public isWorkSubmitted;

    event PaymentReleased(address recipient, uint256 amount);
    event DisputeFiled(address filer);
    event WorkSubmitted(address submitter);

    modifier onlyClient() {
        require(msg.sender == client, "Only client");
        _;
    }

    modifier onlyFreelancer() {
        require(msg.sender == freelancer, "Only freelancer");
        _;
    }

    constructor(address _freelancer) payable {
        require(_freelancer != address(0), "Invalid freelancer address");
        client = msg.sender;
        freelancer = _freelancer;
        originalPaymentAmount = msg.value;
        depositTimestamp = block.timestamp;
    }

    function daysSinceDeposited() public view returns (uint256) {
        return (block.timestamp - depositTimestamp) / 1 days;
    }

    function isPaymentReleaseAllowed() public view returns (bool) {
        if (isDisputeActive) return false;
        return true;
    }

    function isDisputeFilingAllowed() public view returns (bool) {
        if (daysSinceDeposited() > DISPUTE_FILING_DEADLINE_DAYS) return false;
        return true;
    }

    function releasePayment(uint256 withdrawalAmount) external onlyClient {
        require(isPaymentReleaseAllowed(), "Dispute active");
        require(withdrawalAmount <= originalPaymentAmount, "Exceeds original payment");
        require(withdrawalAmount <= address(this).balance, "Insufficient balance");
        (bool success, ) = payable(freelancer).call{value: withdrawalAmount}("");
        require(success, "Transfer failed");
        emit PaymentReleased(freelancer, withdrawalAmount);
    }

    function fileDispute() external {
        require(
            msg.sender == client || msg.sender == freelancer,
            "Only client or freelancer"
        );
        require(isDisputeFilingAllowed(), "Dispute filing period expired");
        require(!isDisputeActive, "Dispute already active");
        isDisputeActive = true;
        emit DisputeFiled(msg.sender);
    }

    function submitWork() external onlyFreelancer {
        require(!isWorkSubmitted, "Already submitted");
        isWorkSubmitted = true;
        emit WorkSubmitted(msg.sender);
    }
}

---

The formal verification spec

Each rule from the English policy maps to a CVL rule that is mathematically proven by the Certora Prover. The comments reference the original rule IDs from the compiled policy.

using FreelanceEscrow as escrow;

methods {
    function isPaymentReleaseAllowed() external returns (bool) envfree;
    function isDisputeFilingAllowed() external returns (bool) envfree;
    function isWorkSubmissionAllowed() external returns (bool) envfree;
    function isDisputeActive() external returns (bool) envfree;
    function daysSinceDeposited() external returns (uint256) envfree;
    function originalPaymentAmount() external returns (uint256) envfree;
    function freelancer() external returns (address) envfree;
    function client() external returns (address) envfree;
    function isWorkSubmitted() external returns (bool) envfree;
    function releasePayment(uint256) external;
    function fileDispute() external;
    function submitWork() external;
}

// Dispute active blocks payment release
rule disputeActiveImpliesPaymentNotAllowed() {
    require escrow.isDisputeActive() == true;
    assert escrow.isPaymentReleaseAllowed() == false,
        "When dispute is active, payment release must not be allowed";
}

// No disputes after 14 days
rule pastDeadlineDisputeNotAllowed() {
    require escrow.daysSinceDeposited() > 14;
    assert escrow.isDisputeFilingAllowed() == false,
        "After 14 days, dispute filing must not be allowed";
}

// Withdrawal cannot exceed original payment
rule withdrawalAmountBounded(uint256 withdrawalAmount) {
    env e;
    require withdrawalAmount > escrow.originalPaymentAmount();
    releasePayment@withrevert(e, withdrawalAmount);
    assert lastReverted,
        "Withdrawal amount must not exceed original payment amount";
}

// Only client can release payment
rule onlyClientCanReleasePayment(uint256 amount) {
    env e;
    require escrow.isPaymentReleaseAllowed() == true;
    require e.msg.sender != escrow.client();
    releasePayment@withrevert(e, amount);
    assert lastReverted,
        "Only CLIENT agent should be able to release payment";
}

// Payment release blocked when not allowed
rule clientCannotReleaseWhenNotAllowed(uint256 amount) {
    env e;
    require escrow.isPaymentReleaseAllowed() == false;
    releasePayment@withrevert(e, amount);
    assert lastReverted,
        "Payment release must revert when not allowed";
}

// Only freelancer can submit work
rule onlyFreelancerCanSubmitWork() {
    env e;
    require escrow.isWorkSubmissionAllowed() == true;
    require e.msg.sender != escrow.freelancer();
    submitWork@withrevert(e);
    assert lastReverted,
        "Only FREELANCER should be able to submit work";
}

// Work submission blocked when not allowed
rule freelancerCannotSubmitWhenNotAllowed() {
    env e;
    require escrow.isWorkSubmissionAllowed() == false;
    submitWork@withrevert(e);
    assert lastReverted,
        "Work submission must revert when not allowed";
}

// Dispute and payment release cannot both be true
invariant disputeAndPaymentMutuallyExclusive()
    !(escrow.isDisputeActive() && escrow.isPaymentReleaseAllowed())

// Dispute filing reverts after deadline
rule fileDisputeRevertsAfterDeadline() {
    env e;
    require escrow.daysSinceDeposited() > 14;
    fileDispute@withrevert(e);
    assert lastReverted,
        "Filing dispute after 14 days must revert";
}

---

Why two rule sets?

The two rule sets are not checking the same thing.

Rule Set 1 asks: "Should this agent do this right now?" Your agent wants to release payment. Before it can, the guardrail checks: is this the client's agent? Is there an active dispute? Has the deadline passed? Is the recipient the right freelancer? This happens in real time, off-chain, on every single action. If any rule is violated, the agent is stopped before it touches the chain.

Rule Set 2 asks: "Can this contract ever behave incorrectly?" The smart contract is verified once, before deployment. A theorem prover mathematically proves it can never violate the policy. No matter what any agent sends it. No matter what order the calls come in. No matter what the inputs are. This isn't a test suite. It's a mathematical proof.

You need both because agents are unpredictable. The guardrail keeps your agent on the rails in real time. The contract guarantees the execution layer is sound even if an agent goes around the guardrail entirely. Neither layer trusts the other. Neither layer trusts the agents.

---

Where the ZK proofs fit

Every time an agent's action is checked, PreFlight returns a ZK proof receipt:

json

{
  "result": "SAT",
  "proof_id": "66839293-5cda-47d4-a142-f01e4f288dff",
  "proof_url": "https://api.icme.io/v1/proof/66839293-5cda-47d4-a142-f01e4f288dff"
}

This is cryptographic evidence that the guardrail checked the action and approved it. The freelancer's agent can verify this proof without re-running the solver, without seeing your policy, and without trusting PreFlight. It just checks the math.

Here's what actually happens when you say "pay the freelancer":

You: "Pay the freelancer for the logo"
        |
        v
Your agent constructs a release action
        |
        v
PreFlight guardrail (Rule Set 1)
  "Should this agent do this right now?"
  Checks: correct agent, no dispute, right recipient, right amount
  -> SAT (allowed)
  -> ZK proof receipt
        |
        v
Your agent submits the transaction + ZK proof to the chain
        |
        v
Verified smart contract (Rule Set 2)
  "Can this contract ever behave incorrectly?" (already proven: no)
  releasePayment() executes on-chain
  Contract enforces: caller == client
  Contract enforces: !isDisputeActive
  Contract enforces: amount <= originalPayment
  -> Funds transfer to freelancer
  -> On-chain record
        |
        v
Freelancer's agent sees the payment
  Verifies the ZK proof (guardrail approved it)
  Verifies the on-chain record (contract executed it)
  Knows the contract was formally verified (it can never be wrong)
  -> Confirms delivery to the freelancer

Three layers of proof. The guardrail approved the action. The contract executed it correctly. The contract itself was proven correct before deployment. The ZK proof lets the other side verify the guardrail check without trusting anyone.

You got your logo. The freelancer got paid. Neither of you read a smart contract. Neither of you trusted the other's agent. The math handled it.

---

Try it yourself

Steps 1 through 3 are available today with any PreFlight API key. Write your policy, compile it, and test it with checkIt.

Step 4, generating formally verified smart contracts from your policy, is in closed beta. If you're building agents that handle real value on-chain, reach out for early access.

Email [email protected] or reach out on X