So I still have no idea how much it might cost. Let's say my contract is 500 LOC and average complexity.
(I'm not convinced formal verification with automated tools can actually substitute for manual audits. I think they're great for augmenting manual audits, but what if there are failure conditions I didn't think to assert as impossible?)
If you see the demo runs on the website FAQ, that example of about 20-50 LoC cost ~$200. You can extrapolate accordingly. Now if you integrate into your CI, I am of course going to only rerun on changes (syntactic, easily checked; and hopefully semantic later.)
If you want a more precise cost analysis, shoot me an email for your specific contract.
And you are right about audits. Except a caveat: The system will by default check for global properties as well, e.g., no double spend. Again, look at the examples in the FAQ. They had no assertions in them. Yet, we find errors.
I make multiple SMT queries. SMT solvers work well in practice, but they are solving a problem which is between NP-Complete to Undecidable (when quantifiers are involved [1]).
Also, we are using a very hand-wavy word definition "complexity of code". This is not the complexity-theory complexity, but instead the types of operations used and the looping/control structure. (In hindsight, I should have used a different word.) So 40 lines of multiple nested loops with multiple hashes being taken and multiple dynamic dispatches over addresses, will take much much longer to analyze than 40 lines of straight line arithmetic.
My tool attempts to guess the estimated runtime midway through the analysis, but there is no real way to accurately estimate the cost upfront. That is why I was saying that if it cost ~$200 for 20-50 LoC then if you accept all caveats then under wildly simplifying assumptions the 500 LoC might take 10x-25x of that cost.
(I'm not convinced formal verification with automated tools can actually substitute for manual audits. I think they're great for augmenting manual audits, but what if there are failure conditions I didn't think to assert as impossible?)