Ethereum is already debating how formal verification should fit into execution and consensus client development. At the application layer, the question reaches beyond a single contract: what would it mean to verify an ERC that different teams are expected to implement?
An ABI can make two implementations callable. It cannot by itself ensure that they agree on success, failure or the state changes a call should produce. In his argument for AI-assisted formal verification, Vitalik stresses that the statement proved must match the statement intended. For an ERC, I read that as making agreement on the intended behavior part of the verification work. Cheaper proofs make an agreed, reviewable specification more valuable.
Regulatory actions on security tokens gave us a concrete example. Take a token already in a RESTRICTED state and two well-formed commands, FREEZE and SEIZE. In the reference model used below, applying FREEZE first lets the following SEIZE finish in SEIZED. In reverse order, SEIZE is rejected from RESTRICTED; FREEZE then leaves the token FROZEN. The same commands produce different final states and outcome traces.
The different outcomes follow from the model’s rules. The standardization question is which rules every implementation must share. Which state is a command allowed to act on? Should a stale command be rejected, reordered or evaluated against current state? Does rejection consume its identifier, and what should an indexer record? Those questions remain even when execution is strictly sequential.
Existing standards deliberately leave some of this meaning open. In the ERC-1400 family, ERC-1644’s controller operation covers recovery and court-ordered transfers; ERC-7943 gives forced transfers a motive-neutral name. ERC-7943 distinguishes freezing from transfer, yet recovery and confiscation can share the same transfer mechanism. A common account of purpose, authority and reversal still needs to be defined in a base interface or extension.
We explored these questions while building ERC-TRUST, a public pre-ERC candidate for typed regulatory actions on security tokens. Its machine-readable kernel generates interfaces and conformance vectors. We connect the model’s conditions to Solidity consumers and tests, check selected compiled-code properties, bind compiler output to runtime bytes, and publish the remaining obligations.
We call this whole-standard assurance: treating the standard’s semantics, generated interfaces, reference implementation, runtime bytes, conformance evidence and remaining assumptions as one auditable chain. We have mechanized semantic and model-level refinement results with artifact-bound implementation evidence. The general runtime-to-model proof remains open. The term describes the scope of the assurance argument, not a completed proof of every link.
Can we make the standard itself falsifiable before its prose is fixed, rather than leaving each implementation to expose its ambiguities later?
1. Can an ERC itself be verified?
EIP-1 describes a Standards Track proposal as having a design document, an implementation, and, where warranted, a formal-specification update. What keeps those parts aligned on the same behavior?
For an application standard, at least six distinct failures are possible.
- The prose can be internally ambiguous. Two implementations may each satisfy a plausible reading while disagreeing on failure ordering, replay, terminality, or event meaning.
- A human-readable interface can drift from its machine form. Function signatures, type widths, domain separators, and receipt preimages can change in one surface without changing another.
- The reference implementation can miss a normative condition. A
MUSTcan exist in the document and have no state-changing consumer in code. - Tests can pass without testing the condition they appear to cover. A branch may be unreachable, a negative may mutate the wrong location, or a verifier may accept stale evidence.
- The runtime identity can drift from the reviewed build. Compiler settings, metadata, immutables, or packaging can change the bytes that actually execute.
- A deployment or profile can claim more than its evidence supports. Interface detection can be true while a privileged bypass, incomplete import, mutable dependency, or missing hook invalidates the advertised conformance class.
These are different failure modes. A theorem about an abstract transition system cannot detect a missing Solidity guard. A Solidity test cannot prove that the natural-language standard chose a coherent transition system. A symbolic execution result over selected paths cannot establish compiler correctness or a deployment address. A deterministic build proves reproducibility of bytes under pinned inputs, not that the bytes implement the right meaning.
A reviewer needs to know which claim each check supports, and which connection still depends on a person’s interpretation.
There is precedent inside the ERC ecosystem for treating conformance as more than interface detection. ERC-6734, for example, defines conformance levels in terms of requirements and test reports, while ERC-7303 publishes a redeployable conformance fixture with positive and negative classifications. A recent thread on this forum argued that conformance at the RPC boundary should be enforceable rather than optional (Ethereum needs Standards-Punk); the argument applies one layer up, to the semantics of privileged application standards. The step explored here is to make the semantic object, generated surfaces, implementation evidence, and unclosed links visible in one package, so a reviewer can challenge each layer without mistaking one for another.
Falsifiability is the useful standard. A claim is falsifiable when a concrete contradictory artifact can cause it to fail. Change a normative identifier without regenerating the interface, and the generator check should fail. Remove a load-bearing guard, and a targeted test or mutation detector should fail. Reuse a receipt for different source bytes, and the identity check should fail. A compatiblity claim should fail when its declared requirements are not met.
A missing condition can have an ordinary, expensive consequence. In Euler’s account of its 2023 exploit, donateToReserves reduced collateral without the health check used by other balance-changing paths. A property requiring donations to preserve solvency at the specified liquidity-check boundary could have exposed that path if it had covered the actual implementation, including deferred checks and price assumptions. An audit or a targeted invariant test could also have caught it. The example supports checking every relevant entry point against the intended rule; it does not establish that our toolchain would have prevented the exploit.
2. Two well-formed commands, two different outcomes
The regulatory-action example is small enough to inspect without a proof assistant. This five-state, seven-label composition model is a foundation model; it is not the current kernel’s full case-and-custody state space. From RESTRICTED, FREEZE moves the asset to FROZEN, while SEIZE is rejected. From FROZEN, SEIZE moves it to SEIZED. These are explicit rules of the chosen model, not facts about every jurisdiction or token.
Figure 1: In the five-state foundation model, reversing FREEZE and SEIZE from RESTRICTED changes both the outcome trace and the final state.
The upper path applies both commands and ends in SEIZED. The lower path records a rejection for SEIZE, keeps the state at RESTRICTED, then applies FREEZE and ends in FROZEN. The model does not silently reorder the queue or reinterpret the first command.
Across all unordered pairs of the seven transition labels, the Isabelle/HOL development classifies twenty-one pairs: twelve commute on final state and nine do not. Each noncommuting pair has a concrete witness state, and the classification is complete for the declared five-state machine. A separate post will examine all twenty-one pairs, their outcome traces, the sixty normal forms of command sequences, and the consequences for security-token state machines. One witness is enough for the present question.
The proof establishes that order can be semantically load-bearing. It does not prove that every ERC must use the same command structure as ERC-TRUST. A standard could impose a global canonical order, give one authority class priority, prohibit concurrent commands, or define a mediation queue. What it cannot safely do is leave the ordering semantics unspecified while claiming uniform outcomes.
ERC-TRUST carries some of those choices into its request types. An action names a case and binds the dependency root and epoch, together with the authority epoch. A reversal also names the action it seeks to undo; its overlay effect or custody record must still be current. Ordinary action requests have no general expected-head field; their case and overlay checks use current state. Stale dependency or authority bindings are rejected. The candidate fixes a common validation prefix, including replay and epoch checks before case-dependent rules, while leaving the order of some later state-dependent failures implementation-defined (request types and validation order).
The theorem tells us that the ordering question matters. Choosing which context to bind, and which differences to permit, still requires a standardization decision.
The action names describe declared legal-effect classes; the machine records an onchain transition. A valid transition does not establish that a court order exists, that an authority acted lawfully, or that beneficial title changed. The model makes this boundary explicit: identical bound inputs produce identical observations even when unobserved external facts differ (paper). The ERC-8320 draft likewise keeps regulated-asset claim anchors onchain while separating them from external truth.
3. From a theorem to a standard obligation
The same separation can be applied to the other semantic results without turning model choices into universal ABI requirements.
| Machine-checked result in the declared models | Design question raised | ERC-TRUST choice | Other possible answers |
|---|---|---|---|
| Command order can change final state and outcome trace | Against which state is a command interpreted? | Case and current-effect checks; dependency and authority epochs; reversals name the prior action | Canonical order, priority rule, mediation queue, concurrency prohibition |
| Rejection and operational failure preserve modeled state but carry different outcomes | Which failures require a new command, and which permit retry? | Typed rejection and operational-failure classes; failed execution writes no contract state or receipt | Another error taxonomy or an authenticated record outside the reverted call |
| A terminal state absorbs later commands; the case model scopes termination per case | What exactly terminates? | Case-local terminality and terminal rejection | Subject-level or global termination, with a different model and explicit consequences |
| Strong states have action-specific origins; removing an overlay can lose earlier history | Which earlier effect does a reversal undo? | Reversals name the original action and check that its effect is still current; prior values support restoration; evidence commitments remain separate from authorization | Explicit restoration targets or another history-carrying structure |
| The same state can accompany distinct attempted-command records in the composition model | How are command identity and observations defined? | Recomputable receipts for successful execution; typed reverts on failure, with no persisted failure receipt | A separately authenticated attempt log with its own guarantees |
These results expose choices a standard needs to make when it adopts this domain and these guarantees. They do not derive universal ERC requirements from one model. In particular, the model’s record of a rejected attempt is not an EVM log: a reverted call cannot retain its own event. An observer that needs a durable history of failed attempts must obtain it outside that reverted execution.
The pattern is especially important for privileged operations. Ordinary token transfers already have a dense body of expectations around balances, allowances, and Transfer events. Regulatory actions add questions that a generic transfer does not answer: which legal-effect class was requested, which authority epoch was used, whether the action can be reversed, whether the case is terminal, which prior action a reversal undoes, and which evidence commitment belongs in the receipt.
An ABI can expose all the necessary functions while leaving those relations implicit. Once multiple implementations, adapters, wallets, indexers, and auditors enter the system, implicit relations become interoperability failures. The values may move correctly while the participants disagree about why they moved, whether the move can be undone, or which record is authoritative.
The semantic contract around the function must be precise enough for independant implementations to expose observable, diagnosable differences instead of silently diverging.
4. How we tried to make the standard falsifiable
ERC-TRUST uses one machine-readable kernel as the normative input for identifiers, command fields, receipt fields, action masks, reversal masks, reason classes, and conformance vectors. The kernel source generates the Solidity interface, ABI, TypeScript types, human-readable kernel rendering, receipt schema, and positive and negative vectors. Continuous checks reject drift in these generated surfaces. The full ERC draft also contains authored requirements and rationale; generation does not establish that every prose requirement has been formalized.
That closes one class of mismatch. It does not prove the semantics, so the abstract state machine lives in Isabelle/HOL. Isabelle checks properties about actions, reversals, replay, epochs, frames, case-local terminality, outcomes, receipts, and the boundary between onchain execution and external facts. It also contains the generated representation of the connection ledger described below.
The Solidity reference then needs evidence about its own behavior.
- Foundry exercises normal paths, rejection paths, operational failures, fuzz properties, and stateful invariants.
- Mutation testing removes or weakens declared consumers and asks whether the named detector actually fails. A killed mutation is evidence about that detector and fault, not proof that the fault model is complete.
- Certora checks four CVL rules for the current ERC-3643 Partial adapter, including that it reports Partial rather than Full and that restriction observations use actual upstream state. Certora also reasons about compiled code; the role described here is the particular rule set we ran.
- Kontrol/KEVM checks four selected high-risk bytecode paths in the native runtime. Our evidence includes no symbolic adapter lane or complete runtime refinement theorem.
- Deterministic builds and runtime binding reproduce the three runtime templates and compare the compiled artifacts in six projections, including ABI, storage layout, creation bytecode, runtime bytecode, method identifiers, and immutable references.
- Independent reproduction recomputes the identifiers and encodings in the 23 published conformance vectors from the specification surfaces. It checks the vector corpus, not every possible input or the endpoint state transitions.
This is a lot of machinery. I would not want every ERC author to repeat the integration work. We chose tools for the questions we needed answered: abstract composition in Isabelle, ordinary execution and fault sensitivity in tests, and selected properties of compiled implementations in the contract verifiers. Their capabilities overlap. The number of tools is a cost of this experiment, not a requirement we propose for standards.
In July, we evaluated Isabelle/Solidity, the recently added AFP framework for specifying and verifying Solidity contracts within Isabelle. It built successfully. Our applicability assessment found that the evaluated version did not supply the source-to-embedding and compiled-runtime correspondence our stateful kernel needed. Its abstract external-call model would still leave our decoding and call/return behavior, including observable outcomes, to be connected separately. Translating pure helpers would not settle those obligations.
There are already approaches that reduce this separation. Act can check EVM bytecode against a high-level specification and export that specification as a transition system to Rocq. That is a serious alternative to maintaining separately related models. We have not tested whether it covers this entire kernel, and have not established that our toolchain is minimal. A smaller toolchain that preserves the claims and exposes its assumptions would be an improvement.
Figure 2: The checks used for each failure mode have limited scopes. Formalization still needs human review, the ledger checks only named obligations, and build identity is separate from semantic correctness. The final two rows identify missing general evidence.
The connecting object is a machine-readable obligation ledger. Every abstract condition named by the ledger must point to four things: a source consumer in the final code, a positive test that activates the branch, a negative detector, and a compiled or downstream consumer. Where a single guard can be removed meaningfully, the negative is a killed mutation. Where removal would not represent the condition, the row names a bounded behavioral negative and its scope.
Figure 3: Artifact relationships in the candidate. The kernel generates the listed interfaces and rendering; authored prose is reviewed separately. Lines for modeling and the obligation ledger show correspondence work, not proved semantic equivalence. The runtime theorem and deployment evidence remain open.
For the obligations it names, the ledger exposes a missing code consumer or detector. Reviewers also classify runtime guards that have no abstract counterpart as runtime-only or as a reason to extend the model. Both inventories are established by review: a requirement omitted from the inventory is invisible to the verifier. This is a useful check on the recorded correspondence, with completeness of the inventory still requiring review.
A proof or test receipt about old source bytes cannot silently qualify new bytes. The index rejects stale receipts against the artifact each binds: formal builds bind the formal root, runtime evidence binds source or runtime identities, and independent reproduction binds vectors. These identities differ because the artifacts answer different questions.
A reviewer can now challenge a specific claimed connection, inspect its evidence, and see whether a repair changed the source that the evidence covers.
5. What is proved, and what remains assumed
At the pinned public snapshot, the twelve declared evidence lanes pass. The ledger has seventy-four rows: seventy closed within the ledger’s scope, two not applicable, and two open rows for the runtime link. The receipts record 121 killed mutations, four Kontrol proofs, four Certora rules and the other checks described above. These figures are evidence inventory counts, not a percentage of a complete proof. The integration guide lists the replay commands. CI reruns some checks and validates the identity of recorded results for others; a green index does not mean every prover and mutation was rerun in that CI job.
The existing Isabelle development includes entrypoint and transaction refinement results within its formal models. It also proves consequences conditional on a connection to runtime execution. The missing runtime_link is that connection: every execution admitted by the selected runtime semantics must correspond to a transaction allowed by the abstract model, including the observed result and state change under the chosen abstraction.
For example, the model may establish that a rejected command preserves balances, case state and replay keys. To carry that result to the compiled contract, we must show that every relevant rejection path implements that behavior, including paths through dependencies. Tests exercise particular executions and the four Kontrol proofs cover selected symbolic obligations. Their success does not establish this general correspondence. In the composition theory, runtime_link is visibly an assumption.
An open link identifies missing evidence, not an impossibility of verification. Proving the compiler correct is one way to transport source-level results. Checking the exact bytecode against the specification can avoid needing a theorem about the whole compiler. Our package has not supplied that general runtime-to-model link; it remains a concrete research target.
The next boundary is deployment. The repository binds source, compiler inputs, and runtime templates, but it claims no chain, address, constructor, role assignment, dependency state, key-management process, proxy, or migration. A real deployment needs a separate manifest and evidence tied to its actual bytes and governance state.
An independent security audit is also absent. The candidate is explicitly unaudited and not for production. Formal proofs can shrink uncertainty about specified properties; they cannot substitute for review of the specification, operational controls, key custody, dependency behavior, or adversarial paths outside the model.
The ERC-3643 profile illustrates why this discipline matters. An earlier profile description was stronger than the implementation behavior supported. The import manifest could verify declared entries without proving that no legacy account had been omitted. Tokens received through an ordinary inbound transfer could remain transferable until the next adapter touch because the upstream token had no same-transaction hook enforcing the adapter-owned frozen target. The current machine-readable profile therefore reports PARTIAL and full = false. The stronger identifier is reserved for a future class requiring an atomic fresh deployment, a complete initial-state gate, and a transfer or Compliance hook in the same transaction (profile definitions).
That correction shows what falsifiability changes. A limitation in prose cannot rescue a machine-readable full = true claim consumed by wallets, registries, or indexers. The claim itself has to become false.
The current permitted summary is deliberately bounded: the abstract model is verified within its declared semantic domain, and the repository provides mapped implementation evidence; end-to-end refinement remains incomplete. The full list of exclusions is public in known limitations.
6. What this could change for Ethereum standards
Solidity’s type checker does not enforce an ERC’s authority policy or lifecycle rules. A program can be well typed while allowing a command the standard intended to forbid. Solidity already has SMTChecker: its CHC engine can reason over unbounded transaction sequences, with require conditions treated as assumptions and assert conditions as proof targets. The remaining work is to specify the right property, account for external calls and supported language semantics, and connect the result to the implementation in use. A missing requirement cannot be recovered just by proving the checks the code already contains.
That makes stronger verification worthwhile for some ERCs, without making a full theorem suite the baseline for every interface. I would choose the depth from what other systems must be able to rely on. The following is a proposed guide, not an official classification or a safety grade for an ERC number.
| Standard surface and examples | Useful evidence | When deeper formal work is warranted |
|---|---|---|
| Identifiers and interface discovery, such as ERC-165 | Precise definitions, canonical fixtures and negative interoperability tests | When discovery is used to authorize a privileged path; interface support alone does not justify it |
| Balances and accounting, such as ERC-20 or ERC-4626 | Conservation and authorization properties; stateful tests with rounding and boundary cases | When asset/share conversions, fees or other composition make local checks insufficient for the claimed invariant |
| Signatures and delegated execution, such as ERC-4337 | An explicit authorization and replay model; evidence for every route that can exercise the authority | When a bypass or cross-context replay can spend another user’s assets |
| Regulatory lifecycle extensions, including TRUST over ERC-7943 and its ERC-3643 profile | A transition model, conflicting-command examples, failure semantics and evidence for the advertised profile | When ordering, reversal or termination must agree across implementations; adapters also need their ownership and hook assumptions checked |
A single implementation can occupy several rows. Even a small interface can authorize a large loss. The table suggests where proof effort is useful; it does not require every listed tool or claim that proofs replace audits.
For the stronger claims in this table, the publication could include:
- A machine-readable normative core for the identifiers, domains, typed outcomes, and canonical preimages that cannot safely drift.
- Generated human and machine surfaces so prose, interfaces, schemas, SDK types, and vectors share one source where feasible.
- Executable conformance vectors with negatives, including stale, malformed, replayed, out-of-order, and unsupported cases.
- Evidence-backed profile declarations whose machine-readable strength becomes false when required conditions are absent.
- An open-obligation ledger linking semantic conditions to implementation consumers while naming every connection still assumed.
- Exact artifact identity separating reviewed source, compiler output, runtime bytes, and deployment state.
There is already a place for formal verification in ERC texts. ERC-7521, like ERC-4337, discusses verification of a central implementation component. ERC-6734 and ERC-7303 provide the conformance precedents noted above. The proposal here is to connect the chosen semantic requirements to generated surfaces and implementation evidence, and publish the unproved connections with them. A precedent that does this better would be useful input to the design.
Editors review the proposed behavior and its claims; implementers and verification teams supply the corresponding artifacts. The community keeps control of normative decisions and can trace them into code.
It also gives disagreements a concrete object. EIP-1 makes authors responsible for building consensus and documenting dissent. Once a requirement is chosen, a reviewer can point to a changed identifier, a missing transition, a failure that now consumes a nonce, or a profile stronger than its evidence.
Ethereum’s standard culture has long valued rough consensus and running code. Whole-standard assurance adds a third question: does the running code preserve the decision the community thought it made?
ERC-TRUST is one public experiment with that question. The domain is unusually demanding because regulatory actions combine authority, irreversible effects, reversals, external evidence, and independent observers. Those pressures made hidden semantic choices visible. The resulting methods may be useful well beyond regulated assets, particularly wherever an ERC exposes privileged state transitions or machine-readable conformance levels.
A separate post will return to the domain in full: all twenty-one action pairs, order-sensitive outcomes, case-local terminality, provenance, sixty normal forms, conformance profiles, and what those dynamics require from a security-token state machine. The method belongs to Ethereum standards broadly. The complete regulatory argument belongs to the asset domain that produced it.
7. Artifacts and decisions for the community
For reproducibility, this post uses the public repository snapshot at commit afde5587. All repository evidence links below are pinned to that snapshot. The linked paper describes kernel version 1; the repository evidence discussed here describes kernel version 2. The main entry points are:
- Pre-ERC draft
- Machine-readable kernel
- Isabelle/HOL session
- Obligation ledger
- Verification summary and integration guide with the replay commands
- Claim matrix and known limitations
- Research paper
Four questions would materially affect how this approach should evolve.
- Ordering semantics. For stateful privileged actions, should a standard bind commands to referenced prior state, specify a global canonical order, or leave ordering to conformance profiles?
- Full-profile evidence. What is the minimum public evidence that should permit a machine-readable Full claim, especially when an adapter depends on an existing token with non-enumerable legacy state?
- Open obligations. Should standards publish unresolved semantic links in a common machine-readable form, or is a prose limitations section the right boundary for ERC process?
- Evidence composition. Could existing specification and bytecode-verification tools share a small artifact format that identifies the requirement, checked program and assumptions, and makes an unresolved runtime correspondence explicit? Which parts could be reused across ERCs?
ERC-TRUST makes the standard’s semantic choices testable and publishes how far their connection to executable code has been checked. The remaining runtime obligation is precise enough to work on. I would like a future ERC author to inherit reusable models of failure and state change, with tools that check their correspondence to compiled implementations and carry the assumptions into deployment evidence. Existing tools already provide parts of that workflow. Can we make that correspondence a normal artifact of an authority-bearing ERC, available before its prose is frozen?