How Good Is Your Formal Specification Mutation Testing To The Rescue!
summary
A tool called Gambit mutation generator automatically creates first-order mutants of Solidity programs by mutating the compiler JSON/AST, compiles and filters them, and runs the same formal spec through the Seer approver for each mutant. A simple mutant flips voted[msg.sender]=true to false and exposes a missing spec rule; adding a property fixes it. Gambit (Rust, open source) also trims ERC‑20 test suites, adds five missing tests, and catches known buggy ERC‑20s while reducing runtime.
AI-written summary · about
chapters (14)
- 0:00Mutation testing for specs
- 3:55Formal verification needs specs
- 5:20Bord voting contract case study
- 8:06Mutation testing and Gambit
- 12:23Fixing spec gaps with Gambit
- 13:24Three ways specs fail
- 15:12Mutant coverage in Gambit
- 19:04Cur uses Gambit in practice
- 20:07Evaluating specs with Gambit
- 20:29Testing suites with Gambit and ERC X
- 21:51Gambit mutants generation
- 23:17Gambit config and Rust benefits
- 24:21Future integrations
- 24:42Summary and Q&A
related talks
27mThe Mutation Game: Cracking the Enigma of Mutation Testing
41mMutation Testing with Mutant
22mKill All Mutants! (Introduction to Mutation Testing)
37mAre your tests good enough?
37mHow to Write Better Code Using Mutation Testing
35mKill All Mutants! (Intro to Mutation Testing)
32mCAN WE WRITE PERFECT TESTS? - MAYBE!
29mKill All Mutants! (Intro to Mutation Testing)