Formalizing Transaction Interpretation

What if we formalized natural language interpretation?

VeryClear won 1st place in Ledger's “Clear Signing, Integrations & Apps” category at ETHGlobal Cannes 2026. We built it in under 36 hours with the ZKNOX team.

For years, signing an Ethereum transaction meant staring at raw calldata, a hex blob that means nothing to a human. Clear signing changed that by translating calldata into sentences like “Approve Uniswap to spend unlimited USDC.”

The ERC-7730 standard has been a major step forward, and adoption is growing fast. But it has two practical limitations. First, most ERC-7730 descriptors are not written by the contract developers themselves. They are contributed by third parties to the Ledger registry, which means the people closest to the code are not the ones describing what it does. Second, when using a hardware wallet like a Ledger, the device fetches the descriptor from Ledger's backend. The user has to trust that backend to serve the correct ERC-7730 file for the contract they are interacting with.

Verity's philosophy is to reduce trust to the simplest possible specification of how a contract behaves. VeryClear applies that idea to clear signing: a short, auditable spec written by the contract developer defines exactly what the wallet is allowed to say, and a ZK proof guarantees it followed the spec.

Specifications as code

VeryClear replaces static JSON descriptors with a small program written in the Verity DSL, an extension of the Lean 4 framework we built for formal verification of smart contracts. A Verity spec can pattern-match on decoded arguments, format token amounts with the right number of decimals, and select different sentences depending on runtime values. A single ERC-7730 entry cannot distinguish an unlimited approval from a bounded one. A Verity spec can.

Because the spec is code, it lives in the same repository as the contract itself. The developer ships the display spec alongside the implementation. The compiler turns it into both an ERC-7730-compatible JSON descriptor and a ZK circuit that proves any wallet follows it exactly.

Example: the full USDC display spec

intent_spec "USDC" where
  const decimals := 6
 
  intent transfer(to : address, amount : uint256) where
    when amount == maxUint256 =>
      emit "Send all USDC to {to}"
    otherwise =>
      emit "Send {amount:fixed decimals} USDC to {to}"
 
  intent approve(spender : address, amount : uint256) where
    when amount == maxUint256 =>
      emit "Approve {spender} to spend unlimited USDC"
    otherwise =>
      emit "Approve {spender} to spend {amount:fixed decimals} USDC"
 
  intent transferFrom(from : address, to : address, amount : uint256) where
    when amount == maxUint256 =>
      emit "Transfer all USDC from {from} to {to}"
    otherwise =>
      emit "Transfer {amount:fixed decimals} USDC from {from} to {to}"
 

The entire display specification for USDC. For each function, list the cases and what the wallet should say.

ERC-7730 (static JSON)

  • One template per selector
  • Cannot branch on parameter values
  • Written by a third-party registry
  • No link to the contract source

Verity DSL (scriptable spec)

  • Pattern-matches on decoded arguments
  • Formats amounts, resolves labels
  • Written by the contract developer
  • Compiles to JSON + ZK circuit

One transaction, end to end

Take a standard ERC-20 approve call on USDC. Here is what the wallet receives, and how VeryClear turns it into a provable claim.

The raw input

0x095ea7b3...
selector: approve(address,uint256)
spender: 0x7a250d5630b4cf539739df2c5dacab4c659f2488
amount:  0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff

A normal wallet pipeline decodes this and asks the user to trust the result. VeryClear treats the result as a claim that must be justified from a public spec.

The USDC spec shown above handles this case. The approve intent checks whether the amount equals maxUint256, picks the unlimited template, and fills in the spender:

1. Decode & evaluate

Parse calldata, run the spec's intent rules, and select the matching template.

2. Prove

Generate a ZK proof binding the calldata to the structured display claim the spec produced.

3. Verify

Check the proof in the browser or on a hardware wallet before signing.

The claim the wallet should be able to justify

{
  contract: "USDC",
  selector: "approve(address,uint256)",
  template: "erc20.approve.unlimited",
  fields: {
    spender: "Uniswap V2 Router",
    token: "USDC"
  },
  display: "Approve Uniswap V2 Router to spend unlimited USDC"
}

The proof certifies that this structured claim is the correct result of evaluating the public spec on the calldata. But the claim is still a template with typed holes. To show a human-readable sentence, the wallet needs to fill those holes with the actual display strings from the spec.

Where the spec text comes from

Once the proof confirms which template matches, the wallet still needs the human-readable text that fills the template. That text lives in the spec itself, so the question becomes: how does the wallet get a spec it can trust?

In our proof of concept, we stored specs directly in an ENS registry we deployed on chain. That works, but it means users trust whoever published the registry entry. A better model would let users review and approve a spec the first time they interact with a new contract. The wallet would show the spec, the user would sign their approval, and that approval would remain valid for a fixed period, say one year. After that, the wallet prompts for re-approval, which also gives spec authors a natural window to publish updates.

Verify it yourself

  1. Open the browser demo and inspect the step-by-step pipeline from spec lookup to proof verification.
  2. Open the hardware demo to see the same display claim checked on a Ledger device.
  3. Read the prototype README for the concrete trust chain: ENS registry, verification-key hash commitment, and storage-proof verification on hardware.

Questions worth asking

Isn’t this still trust, just moved somewhere else?

Yes, and that is the point. Trust moves from a large, opaque software stack to a small public specification that can be reviewed, versioned, and audited by people other than the wallet vendor.

Does VeryClear solve the natural-language problem?

The proof guarantees the wallet followed the spec. Whether the spec says the right thing to a human is a separate problem. That is why we think specs should be written by the contract developers themselves, reviewed publicly, and approved explicitly by users. The next open question is connecting these display specs to the formal proofs of the contract itself, so that the sentence the user reads is consistent with the verified behavior of the code.

Can this work in languages other than English?

Yes. The proof validates the template structure, not the display strings. A French-speaking user could approve a French translation of the same spec. The ZK circuit is identical; only the human-readable text changes.

Links

ETHGlobal showcase

ZKNOX write-up on hardware-verified clear signing