Aave V4 spokes enable easy deployment of various lending markets, each with different collateral management, risk premiums, liquidations, per reserve risk configuration, and oracle integration, without having to manually manage liquidity. We show how to leverage agents to develop new secure spokes. The core idea is that the user provides an informal definition of correctness for these applications. Our agentic pipeline translates these informal definitions into a formal specification of the application’s safety properties/invariants. Once we have these formal specifications, we can Vibe-code the spoke implementation guardrail with the Certora Prover. The LLM cannot introduce bugs into our generated implementation because the Certora Prover will reject any potential implementation that does not satisfy the formal specification.