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/