Since I started working with smart contracts a few years ago I’ve had linear temporal logics (LTL) in my mind as an ideal interface to gain confidence about them. So, while researching verification tools, VerX caught my attention, but sadly it’s a private tool out of our reach for now.
On their paper they comment how previous work determined that a particular type of LTL predicates, Past LTL, can be reduced to reachability checks, commonly expressed as assertions in the code. That made me think the same instrumentation could be useful for all kinds of analysis tools. Thus, providing a friendly interface with temporal operators for developers to define their project’s requirements and taking advantage of all the verification tools out there and to come. For instance, you could use a fuzzer or a symbolic executer during development to aim at instant feedback about “easy to find” bugs, and later run heavyweight analysis tools like abstract interpreters or model checkers to get a full or partial proof, and more complex counterexamples.
In the VeriMan repository you can find the prototype that I’ve put together in a few weeks, with more information on it’s usage. It also allows you to generate Echidna invariants and to directly feed the instrumented contract to VeriSol, and even to Manticore if you want blockchain-ready counterexamples. I decided to specially support these tools because of our experience while researching, mostly illustrated on my forum post analyzing the MakerDAO contracts, but many other tools are implicitly supported, like Mythril.
I’m looking forward to any feedback or questions you might have 