One post tagged with "metamorphic-testing"

Miscompilations and semantic drifts are bugs where the compiler accepts a valid program and silently emits code that behaves differently. On smart-contract platforms this is the bug class that can drain user funds. The post covers differential testing, metamorphic mutations and their sound synthesis — each mutation is proven equivalence-preserving in the developed framework written in Lean4. We will also discuss some of the miscompilations found, some of which resulted in bug bounties.