Verifying Rust: Exploring Verification Options for Substrate

I’ve recently been playing around with three verification tools and tried applying them to substrate:

  • kani
  • Prusti

See my blog post here: Verifying Rust: Exploring Verification Options for Substrate | Navigating Blocks and Chains

I did not get very far yet to produce quite meaningful results apart from knowing that we don’t have panics in our on-chain code base (which is something I guess). My next step will be to write conditions around the code base to do more meaningful verification.

If anyone else is also interested in code analysis, would be great if you could share your experience.


In the runtime yes we do not have panics as panicks can cause flooding the chain with failing txn and not paying the fees.

Hi @dom. Just to already share our RFP here. Let me know if you know someone who might want to work on this. Or if you want to work on it yourself.
Bhargav, who mainly wrote it, also will reply here. In the meantime, you can take a look at his example here. We are also quite interested in this, and I think it would be super useful for the ecosystem.

1 Like

Hi @dom
Thanks for sharing the blog, quite interesting.

We at W3F have been working on a feasibility study on Static Analysers for Rust. The objectives are two-fold:

  • Determine interesting classes of bugs/vulnerabilities which can be detected using static analysis and verification techniques with reasonable soundness guarantees.
  • Identify robust tools on top of which Substrate-specific static analysis features can be built on.

This is still WIP, but so far our experience has been quite positive with MIRAI (abstract interpreter) and Crux-MIR (symbolic execution engine). Here is my fork of MIRAI tuned for Substrate.

MIRAI throws several warnings related to unsafe math operations, and potential memory-related panics. However, the false positive rate is significant (on a small sample). To reduce False positives, we ideally want to develop a hybrid tool that performs Symbolic execution on the warnings generated by abstract interpretation. This will also give us concrete tests that trigger the warnings and also help in triaging the bug.

Another line of work is to use the Tag and Taint analysis framework of MIRAI. Several susbtrate specific vulnerabilities could be modelled as sink-source dataflow properties, and the custom tags can be defined to track its flow. This RFP provides more information. We have been in touch with developers of MIRAI and they are willing to support specific request on the tool side, if any.


Thanks @David @bhargavbh !

Fully agree with your goals. To me, there are two parts to the verification aspect that are of particular interest:

  1. Absence of common vulnerabilities. That seems very close to what your RFP is looking for. Trail of Bits also just released common vulnerabilities they found in substrate: Substrate - Building Secure Contracts. The out-of-the-box MIRAI actually did not give me false positives on our runtime crates. Will take a look at your fork next.
  2. Verification of invariants/properties of the implemented protocol. I’m aware of the Hydra team using proptest already on their implementations and find this a very good example how I would want to work with MIRAI (or other tools) to reason about code: HydraDX-math/ at 36432a1b139400eb69b096c32af488d3cf4b20c2 · galacticcouncil/HydraDX-math · GitHub

Will share my progress here. The main focus for me (or us at Interlay) will be on the protocol properties first.


Interesting topic, I think adjusting those low-level tools to work with Substrate is highly valuable.

For the sake of completeness, Subtrace is a linter that helps avoiding common errors.


Hey @dom! I’m curious about what sort of interface you would like for verification.

We’re working on a project to build a Rust verification tool based on verifying MIR. So far, we’ve been thinknig that we plug into property testing framework at Rust level (like what HydraDX is using), so that users can write property tests that are fuzzed at the rust level, then verified using our tools and symbolic execution.

We’ve actually had pretty good luck with doing the same for Solidity → EVM: evm-semantics/ at a476711cd3336c7574fd86960fc002fc39eafc6b · runtimeverification/evm-semantics · GitHub. These property tests can be actually quite expressive, even capturing many contract invariants: v2-foundry/InvariantsTests.t.sol at f4a60d6363ada8b9648ab57df42618a4647fb12d · alchemix-finance/v2-foundry · GitHub. Nice thing is no other specification language to learn.

Anyway, we’re early stages in building this out, so curious about what you’ve learned about verification interfaces in your study so far.

Hi @ehildenb!

Interface-wise, I was thinking mostly along the lines of something that runs in the rust toolchain (like MIRAIs cargo mirai) and writing the checks in rust itself.

I like what you linked here: v2-foundry/InvariantsTests.t.sol at f4a60d6363ada8b9648ab57df42618a4647fb12d · alchemix-finance/v2-foundry · GitHub. This is what I had in mind as well! In my (very limited) experience trying out verification languages, they tend to come with their own issues and especially rust has so many helpful tools/useful compiler errors that staying in that ecosystem would make it most helpful.

Do you already have some code/links of your work on MIR?

Hi @dom,

I also work on the project with @ehildenb, I wonder what your thoughts are on an interface with refinement types. There already exists a tool Flux that provides refinement types as annotations to Rust projects.

Here is a online editor where you can interact with the examples they have:

Any feedback is appreciated