Alfred

Alfred is an agentic auditor of smart contracts on the EVM and activated in your IDE of choice. It makes formal verification with Cetora easy by discovering invariants, generating specs, and explaining proof failures.