Gandy: Neurosymbolic Smart Contract Verification

Most Web3 security tools rely on static analysis or pattern matching to catch known vulnerabilities like reentrancy. However, the most devastating hacks in decentralized finance—such as the $182M Beanstalk exploit—are not simple bugs in the code. They are fundamental flaws in the mechanism design and game theory of the protocol. Gandy is a revolutionary CI/CD platform that verifies the economics of your smart contracts, not just the syntax. Built specifically for the IBM Bob hackathon, Gandy introduces a true neurosymbolic verification loop to Web3 security. Here is how the loop works: Intent Analysis: IBM Bob (powered by Watsonx) reads raw Solidity code from a GitHub PR and extracts the economic rules and developer intent. Formal Verification: Bob translates the code into an SMT-LIB2 specification, which is mathematically proven against core financial invariants using the Z3 solver. Game Theoretic Modeling: The system uses Nashpy to model the rational behavior of attackers. If an exploit strategy becomes a dominant Nash equilibrium, Gandy flags the attack as inevitable. Auto-Patching: When a vulnerability is found, IBM Bob generates a secure patch. Gandy then re-analyzes the patched code to mathematically prove the exploit has been neutralized. For our hackathon proof-of-concept, we ran Gandy against the exact Beanstalk Governance contract from before its $182M hack. Gandy successfully mapped the flash-loan voting attack, flagged the Nash equilibrium dominance, and auto-generated a secure patch. By combining the linguistic reasoning capabilities of IBM Bob with rigorous mathematical solvers, Gandy ensures that protocols are structurally and economically secure before they ever reach the blockchain