Composing EVM Smart Contracts: A Seam Calculus

Many high-impact failures in composed Ethereum applications arise not inside a single contract but at the seam where one component silently assumes behaviour a neighbour does not guarantee. This working paper gives such boundaries a precise calculus — separating specification conflict from seam non-conformance, proving a one-directional rely–guarantee soundness theorem, and turning the assume–guarantee ledger into a typed, finite graph. It applies the calculus to load-bearing EVM standards, six DeFi platforms, and a fully worked yield-router case study.

GitHub

Composing EVM Smart Contracts: A Seam Calculus

A precise calculus for the seams where composed EVM applications fail — separating specification conflict from seam non-conformance, with a one-directional rely–guarantee soundness theorem and a typed assume–guarantee ledger applied to load-bearing EVM standards, six DeFi platforms, and a worked yield-router case study. (IEI working paper · research repository on GitHub.)

Open original ↗