A builder who wants more than a written code review can ask whether stated contract properties actually hold. An article published on 11 November 2026 at 13:02 (UTC+8) describes AI formal verification for that task. Original: 智能合约的 AI 形式化验证：成本与使用场景.
What the agent hands the prover
The article describes an AI agent that reads contract code and documentation, infers properties and invariants, and generates a formal specification together with verification rules. Those rules are then passed to a prover.
Here, a property is a claim the contract is supposed to satisfy, and an invariant is a claim that should remain true as contract state changes. The prover’s answer is not always definite:
- If a check fails, the prover supplies a counterexample.
- If the check times out, or resources are insufficient, the result is uncertain.
Review notes and checked rules
The article contrasts AI code review with AI formal verification by the kind of evidence each produces. A review is an assessment of the code. Formal verification, as described, is a prover’s check of generated rules, which may end as a successful proof, a counterexample, or an uncertain result.
The article says AI can reduce the cost of writing specifications and of proof engineering. It also states two limits. A specification may omit a requirement, so a proof covers only what was written down. Complex properties still need an expert.
The Aave V4 Hub experiment
The article reports a Certora AutoProver experiment on the Aave V4 Hub. In that run the tool generated 104 rules and proved some properties. It did not prove share-value monotonicity. The article also lists use cases, costs, and pricing.
For a builder learning the workflow, the observable result is the prover’s outcome on a stated rule: proved, failed with a counterexample, or left uncertain. A requirement that never made it into the specification is not established by proofs of other rules, and a property the prover did not prove remains unproved.