basedcryptoji/solvr-aeon-skill

This repository is a skill pack for AEON, an autonomous agent runner, that plugs into a service called Solvr. Solvr provides live intelligence about contracts deployed on Base, a blockchain network. The pack adds one skill, called formal-verification, which produces a work order for proving that a smart contract behaves as intended. The motivation is taken from a Vitalik Buterin essay published in May 2026. The argument is that AI can find bugs in code faster than humans can patch them, so trustless code looks doomed. The counter-move is AI-assisted formal verification, where the bottleneck is not writing proofs but stating the right theorems against the right adversary model with accurate context about what the contract really does. Solvr's intel layer is meant to fill that context gap. Given a Base contract address, the skill generates a complete work order: a list of theorems anchored to live intel and security flags, a Lean 4 spec skeleton, an assumptions section, a residual-risk report, and a human audit checklist. The output is then handed to a proof-trained model such as Leanstral, Lean Copilot, or DeepSeek-Math, or to a human prover. The skill itself does not compile Lean, submit transactions, or execute bytecode. Setup involves staking 20 million SOLVR tokens on Base to unlock the Standard tier, generating an API key on the Solvr dashboard, and adding that key as a repo secret. The skill is then enabled in an aeon.yml file and triggered manually from the AEON dashboard with the contract address as a variable. The API key is read-only and cannot sign transactions or move funds. The README spends time on the security model, listing threats like contract-address injection, prompt injection from API responses, bearer-token exfiltration, hanging requests, and scope creep, with the mitigations used for each. Limits noted include hidden assumptions and the gap between proving source and proving compiled bytecode.