works on
ethereum virtual machine 1formal verification 1large language models 1lean theorem prover 1refinement proofs 1smart contracts 1

From the 1 of 1 linked paper with an AI index.

collaborators

1 paper

cs.PL2026

Foundational Refinement Proofs for Deployed Bytecode, at the Price of Tokens

Lefteris Lazaropoulos, Zoe Paraskevopoulou

The paper presents EquiVM, a Lean-based framework that uses large language models to automatically generate machine‑checked refinement proofs linking deployed Ethereum bytecode to…