Verifying LLM powered Code Transformations with Equivalence Checking
summary
Certora builds Concordance: feed complex Solidity (often inline assembly) to an LLM to generate a simplified implementation, then run equivalence checking via a symbolic SMT-based prover that instruments bytecode, hashes observable side effects (calls, logs, storage, return/revert) and over-approximates external calls. Concordance iterates with the LLM until the prover finds equivalence or a counterexample (e.g., a malformed ABI boolean causing different revert data), and it has even found a real Vyper compiler optimization bug. Concordance runs and returns concrete counterexamples for fixes.
AI-written summary · about
chapters (15)
- 0:00Verifying LLM code transformations
- 1:06Inline assembly in Solidity
- 2:29AI code rewriting with LLMs
- 3:53Trusting AI with equivalence checking
- 4:56Program equivalence in smart contracts
- 7:02Equivalence with environment state
- 8:07Side effects and observable behavior
- 10:57Contract equivalence definition
- 11:59Concord formal verification
- 14:23Bytecode instrumentation for side effects
- 17:34Concord validation and applications
- 18:56Concord tool feedback loop
- 21:05Prompt engineering for LLMs
- 22:08Open source limitations
- 22:29Q&A gas efficiency and hallucinations
related talks
23mUsing LLM Generated Formal Specs to Prevent the Next DeFi Hack
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
06mFormal Verification with the Certora Prover
40mSafe Coding with LLMs - Verifiable Scala Silver Bullet
01h 17mProof-Carrying Code For the Age of AI: Machine-Checked Guarantees from(…)
32mVerifying Constant-Time Implementations
33mCorrectness Too Cheap To Meter: Formal Verification and LLMs
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems