All problems
Cybersecurity
Formal Verification of Smart Contract Compositions
Code: ANX-RP-008
Develop automated formal verification tools that can prove safety properties of composed smart contracts across DeFi protocols.
Why it matters
DeFi protocols compose like Lego blocks. A vulnerability in one contract can cascade across the entire ecosystem, as seen in billion-dollar hacks.
Research gap
Current verification tools analyze individual contracts in isolation, missing cross-contract reentrancy and state inconsistency bugs.
Research questions
- 01 How do we model cross-contract state transitions formally?
- 02 Can we scale model checking to compositions of 100+ contracts?
- 03 What abstraction techniques make verification tractable for gas-optimized code?
Suggested technologies
Required skills
Team and supervisor
2-3 researchers, supervised by Muhammad Qasim.
Suitable for: CS, SE.
Expected deliverables
- Verification tool for cross-contract properties
- Case studies on major DeFi protocols
- Automated bug discovery pipeline
Work on this problem
Apply to the lab and this problem becomes your supervised research project.