Formal verification of Clarity based smart contracts

[hassan-truscova]

Hi Everyone,
My name is Hassan from Truscova GmbH.
Recently, I was looking at the verification/testing tooling for Clarity based smart contracts, in particular related to fuzzing, symbolic execution, and formal verification (model checking, theorem proving) etc, however, i could not find much.

The good thing is that i got in contact with @moodmosaic via his Blog article. He was kind enough to respond to my emails and for a very helpful discussion. He also introduced me to rendezvous for fuzzing the heck out of the Clarity-based smart contracts, which is pretty cool.

I wanted to know if there is any interest or if there are any tools for doing formal verification of Clarity-based smart contracts? or if anyone is already doing it?
Any leads, contacts, connections would be really helpful :)

Thank you very much in advance.

[jcnelson]

Hi there! I see you've been in touch with @moodmosaic elsewhere.

I think there is interest in formal verification, and as far as I know, no one is doing it yet. This is currently impeded by the lack of a formal language specification. AFAIK, there isn't even a grammar written down yet. But because Clarity is a (comparatively speaking) very simple language, it shouldn't be an insurmountable task to write a correct one; it's just that the core blockchain devs have been tied up until recently with shipping and stabilizing Nakamoto.

If this is something you'd like to pursue, the best people to talk to are @kantai and @obycode.

[hassan-truscova]

Hi @jcnelson, thank you very much for the response. If there is interest in formal verification, i would be very interested in knowing more about what opportunities exist. Do i need to send PMs to @kantai and @obycode ?

[moodmosaic]

This could be valuable for fuzzing tools like rendezvous. While rendezvous tests properties probabilistically, formal verification would check all paths exhaustively. Another use case would be enabling systematic reasoning about AST nodes, making it easier to compute min/max runtime costs, as discussed in #5360 (comment). There are likely other use cases worth exploring too.

[atifhass]

Hello @hassan-truscova @moodmosaic @kantai @obycode

We've developed some tools that we’re currently testing out internally and with some friendly users that are specifically addressing formal verification and audits in general. We’ve developed two tools:

• **Formal Verification Tool - A SMT based Bounded Model Checking(BMC) engine
• AI Audit Agent - Smart Code Scan powered by leveraging fine-tuned LLMs which scans for vulnerabilities and potential bugs**

Here’s a link to our demo youtube video. link

We'd love to hear your feedback and offer a live demo to test these features. Let us know how you would like us to set up your accounts to try out the tools!

Learn more about Clara at - https://www.goclara.ai/

[atifhass]

@moodmosaic adding you to the event

[BowTiedRadone]

@atifhass works for me!

[BowTiedRadone]

Got the invite. Thank you! Looking forward for the demo! 🚀

[hassan-truscova]

@atifhass @BowTiedRadone @moodmosaic thank you very much for attending and presenting the demo. For me personally, it is always nice to see formal verification being used in industry :) Having said that, @atifhass, during the demo your colleague mentioned that maybe you will make the reports publicly available. Is there any timeline for that?

Secondly, given that there is a fuzzing tool (Rendezvous) already available, is it possible for you guys to make a sliced or limited version of your formal engine available so that i can also do some benchmarking?

third, you mentioned during the demo that you are running into some issues related to mappings and iterative structures. Would you be open to have another discussion? maybe i can help you guys there.

Looking forward.

[mali-tintash]

@hassan-truscova ,
@moodmosaic @BowTiedRadone and Rapha. Thank you guys for taking the time out for the demo presentation.

@hassan-truscova , regarding issues related to mappings of iterative structures @atifhass will coordinate with you . Thank you for agreeing to help us around that.
We are in the process of making it CLI friendly. We'd be happy to share it with you for feedback and improvements.

The reports and the target file are attached below
Audit Report.pdf
Formal Verification Report.pdf
target_original.zip