We pointed AutoProver at the Aave v4 Hub, gave it none of our work, and let it write its own spec. It came back with the Hub's solvency invariant: a share is always worth at least one asset. That is the same property we had written by hand as P-06, and it is not a small thing to arrive at unaided.

It also went to real lengths to prove it. That invariant does not go through if you just hand it to the Prover, and AutoProver did the kind of work we would have done to get it through.

What the run did not produce is a rule for the other half of P-06: that the share price never goes down. Those two sound like the same property. They catch different bugs. The floor catches one of the issues we reported on the Hub. The monotonicity catches the other, and nothing AutoProver proved would have caught it.

AutoProver will hand you a large body of true, checkable rules about a contract, including substantial ones. However, it is not yet a perfect oracle of your intent. One still has to make sure the most relevant properties to a protocol’s safety are verified.

Both of us wrote solvency

Here is what AutoProver wrote, out of the generated spec file:

/// Core (inductive) form of Property 20: the added-share price
/// is never below one asset per share, measured on the stored
/// ledger. Because the statement is `addedShares + realizedFees
/// <= liquidity + swept + owed`, it also entails that
/// `totalAddedAssets` never underflows.
invariant added_shares_do_not_exceed_total_added_assets(uint256 assetId)
    currentContract._assets[assetId].addedShares
        <= totalAddedAssetsStored(assetId)

Certora wrote this as P-06, totalAssetsVsShares: "The sum of added assets is greater than or equal to the sum of added shares." Solvency is the property every lending protocol should have, everybody who ever worked on one knows to look for it, and the Hub's ledger tells you what the terms have to be. Any serious work on Hub.sol has to reason about solvency.

AutoProver did not simply see the property and translate it. It came up with the invariant itself and then built the proof around it, automatically.

The same goes for other properties. It wrote the five invariants saying each asset-level total equals the sum of its per-spoke rows, which together are our manually derived P-05. It wrote the four field bounds those five invariants stand on: the drawn index never below RAY on a listed asset, the liquidity fee no greater than 100%, an asset id listed exactly when it sits below the asset count, premium offset never above premium shares. Those properties together are our P-04. It also proved that the Hub's token balance covers each asset's recorded liquidity, which is our solvency_external.

The more interesting part is not just that it found the same properties. It also found the same dependency graph. The five requireInvariant lines inside its solvency proof are exactly our field-integrity group. It worked out that the solvency bound rests on those four facts, which you usually learn by watching a proof fail, spending iterations, work, and time. AutoProver automates the iterative process, freeing our time to do higher-level thinking on protocol correctness.

It can do the hard proofs

A seemingly simple and intuitive property may have a complex justification. 

addedShares <= totalAddedAssets does not verify if you hand it over as written. The query has to reason about interest growing the index and about the operation's own share arithmetic at once, and it dies on add, remove, draw and restore. Three things AutoProver did about that:

It split the proof. Every mutating Hub entry point is accrue(); op();, so the transition factors in two. Assume the asset is already accrued and the leading accrue() collapses, leaving the Prover only the operation. The accrual half becomes its own rule, accrual_preserves_added_shares_bound. A third rule lifts the result from the stored ledger to the number getAddedAssets actually returns. Three entry points never call accrue() at all, so they get their own preserved blocks.

It checked whether its own rule proved anything. The lifting rule is gated on requiring !lastReverted, which is exactly the shape that passes for free if the call always reverts. The spec says so, and says where the real justification sits instead:

"the lifting rule below is gated on !lastReverted, so the no-underflow content at the accrued index is carried by accrual_preserves_added_shares_bound, whose right hand side is pure mathint arithmetic and therefore cannot be vacuously satisfied."

It got around the assembly. The four SharesMath helpers are re-implemented exactly in CVL, pinning each quotient with two-sided multiplicative constraints instead of dividing, which sidesteps OpenZeppelin's 512-bit Math.mulDiv assembly and hands the solver the product facts the share-price argument needs. Its own note: "it was what finally made eliminateDeficit verify."

So this is not a tool that can only state the easy things. It did the kind of proof work we would normally have expected to do ourselves. The next section is about a property AutoProver identified and tried to prove, but could not finish within the available budget.

The rule it could not finish

P-06 has two halves. The basis, which AutoProver proved. And supplyExchangeRateIsMonotonic: the share price never decreases. AutoProver identified and formalized this property too, but the proof ran past the available budget before it could finish. AutoProver states the property explicitly:

“For every listed asset, the supply share price (totalAddedAssets() + SharesMath.VIRTUAL_ASSETS) / (asset.addedShares + SharesMath.VIRTUAL_SHARES) never decreases as a result of any externally callable function: add, remove, draw, restore, reportDeficit, eliminateDeficit, refreshPremium, transferShares, payFeeShares, mintFeeShares, sweep, reclaim, addSpoke/updateSpokeConfig/updateAssetConfig/setInterestRateData, or interest accrual.”

This property is important. Both of the rate findings we reported on the Hub are violating the monotonicity property, and only one of them is also violating the basis.

M-02 broke both. totalAddedAssets used to round up in two places independently, and reportDeficit moves value across them, so the total could come out smaller after the move than before. That pushes the price below one, so the base solvency property catches it. AutoProver's proven invariant would have caught this.

M-01 broke only monotonicity. getFeeShares() computed the fee like this:

uint256 feesAmount = indexDelta
  .rayMulDown(asset.baseDrawnShares + asset.premiumDrawnShares)
  .percentMulDown(liquidityFee);

It rounds down over the combined base and premium drawn shares, while totalDebt computes the two separately. The two paths disagree about rounding, so accruing interest could shave value off shareholders. It never drops the price under one. It just moves it the wrong way, a little, on the fee path. The base solvency property is blind to it.

That is the gap between the two halves, and it is not a mere minor technicality. A protocol can sit comfortably above one asset per share forever while leaking value out of holders on individual transactions. The basic solvency is the sanity check. Monotonicity is the validation.

Nothing about writing it is hard, either. Read the rate, call the method, read the rate again, assert it did not fall. The hard part is deciding that this is the rate that must never move down, and noticing that the fee path and debt path disagree about rounding. That decision comes from asking what the protocol owes its users, and it does not spelled out in the source code. AutoProver automatically reached this (correct) decision, but failed to finish the proof due to technical limitations in our beta.

Coverage is not the job

The run came back with 104 rules. Most of them are true, checkable, and not particularly sexy: registry entries are well formed, unlisted slots are empty, config setters write the field they claim to write. Good things to know. They are not the properties you would build an engagement around, but they are still useful to have checked.

Having these essential correctness properties of your system proven before an audit or formal verification engagement is useful. It enables an engagement to focus on making sure no critical property is missing. 

A verification engagement is not for producing a list of rules. It is about identifying precisely the handful of invariants that have to hold for a protocol and the people using it to be economically safe, and then proving those. On the Hub that meant deciding the supply rate must be monotonic and not merely bounded, that rounding has to agree across every path touching the same quantity, and that adding a spoke twice must not be allowed to silently zero a live position. Three findings came out of those three decisions.

Where AutoProver is the right call

If a protocol has no formal verification at all, this is a strong first move and we would say so to anyone. You get a large body of machine-checked properties about your actual code, in hours, with no specification effort on your side, on whatever commit you are on today. You do not have to be a formal verification expert to get a decent verification suite immediately. Furthermore, it is a reasonable base to build upon later, whether you look to expand on the coverage or to build more code.

If what you need is assurance about the specific ways your protocol can lose money, the generated spec is a starting point, not the whole answer. A professional verification engagement still needs to identify the properties that matter most, work out what is missing, and prove them. Running AutoProver first makes that engagement shorter, smoother, and more focused. On the Hub, it had already done a significant amount of the work before the researcher got involved. Instead of starting with a blank spec, we had a large set of machine checked properties to work from, including the solvency invariant and the supporting rules it depended on.

Point it at your own code. AutoProver is in the Certora platform. The useful way to judge it is on a contract you know: read the spec it writes and see whether the properties you care most about are in there. We are continuously improving AutoProver to cover harder and more impactful properties. Come talk to us and we will find the best way to help you deliver securely.