Add native Clarity fuzzing for sBTC contracts

[moodmosaic]

This adds native, Clarity-based fuzzing for the sBTC contracts, inspired by prior work in stacks-core#4550 and stacks-core#4842.

The approach is similar to Echidna and Foundry but uses Rendezvous, a forthcoming tool for Clarity fuzzing. This PR will move out of draft once Rendezvous is publicly available and all sBTC contracts are covered.

[moodmosaic]

Taking the PR out of draft state now that rendezvous has been open-sourced (see stx-labs/clarinet#398 (comment)).

[djordon]

This PR doesn't seem to include any of the necessary testing/fuzzing logic. @moodmosaic Do you plan on adding that here?

[moodmosaic]

This PR actually does that logic through the .tests.clar files. Rendezvous (rv) works differently from traditional fuzzers - it uses the test files we've added to perform both property-based testing and invariant testing.

To clarify:

1. The .tests.clar files contain both invariants (e.g., invariant-signers-always-protocol-caller) and property tests (e.g., test-withdrawal-req-id-incremented). These declarations are what rv uses as the specification for fuzzing.

2. rv specifically fuzzes at the invariant level to help/make sure contract state remains valid under various conditions. This aims to detect state consistency issues early. Consider the PoX-2 stack-increase bug - while rv didn't exist then, tools like this aim to reduce the risk of such critical bugs. This example demonstrates this approach.

3. One reason we opened this PR is to test rv with real codebases. It's working probabilistically for now - we don't exhaustively explore all possible cases (though we plan to support that via MiniZinc models).

4. Rendezvous also supports traditional function-level fuzzing to prevent panics and unhandled errors, though without coverage information it's not as efficient as LLVM/clang fuzzing tools. We have an open issue to help move forward with this.

For context, this technique has already proven valuable - a few issues in PoX-4 were identified and addressed before it went on mainnet. The Rust equivalent would be something like adding madhouse-rs for stateful fuzzing, as shown in #1633.

Note that we didn't complete all .tests.clar files in this PR as we didn't receive feedback at the time and had to prioritize other work. If by fuzzing you meant something else or expected a different approach, happy to clarify or adjust the PR as needed. 🙏

[BowTiedRadone]

Hi @aldur @djordon @setzeus! 👋

Just updated the Rendezvous tests to the current logic of the sBTC contracts. Some invariants and properties are simple, establishing a set of must-have sanity checks while showcasing the principles and features of the tool @moodmosaic and I built.

For a better review experience, I've added some comments to sbtc-registry.tests.clar that explain the two testing types (invariant and property testing) and every single test. Did not extend the comments to the other test files until you agree with their language, style, etc.

Quick guide on how to run all the possible test suites locally:

cd contracts
npm i
npx rv . sbtc-registry invariant
npx rv . sbtc-registry test
npx rv . sbtc-token invariant
npx rv . sbtc-token test
npx rv . sbtc-withdrawal test

To increase the number of runs of a testing routine (100 by default), you can use:

npx rv . sbtc-registry invariant --runs=1000

On failure (shouldn't be the case at this point), a seed is reported at the end of the run. You can use that seed to reproduce the exact same sequence of events:

npx rv . sbtc-registry invariant --seed=<REPRO_SEED>

There are more advanced features in Rendezvous, but I'd stick to the basics until common ground is settled. 🙌

For all features explained in detail you can check Rendezvous Book 📖

[moodmosaic]

/cc @djordon @aldur — are you interested in this? Should I keep open for a longer time?

[setzeus]

Hi hi gentlemen! Deeply appreciative of the hard work here - thank you for that penultimate comment with testing instructions.

Giving it a whirl this weekend & will come back with additional thoughts / requests (or a good ole' LGTM).

[setzeus]

Hi @moodmosaic @BowTiedRadone, I tried running the tests following the instructions above & get the following:

setzeus@MacBookPro contracts % npx rv . sbtc-registry invariant
npm ERR! could not determine executable to run

npm ERR! A complete log of this run can be found in:
npm ERR!     /Users/setzeus/.npm/_logs/2025-06-28T13_30_26_852Z-debug-0.log
setzeus@MacBookPro contracts % npx rv . sbtc-registry test
npm ERR! could not determine executable to run

npm ERR! A complete log of this run can be found in:
npm ERR!     /Users/setzeus/.npm/_logs/2025-06-28T13_30_41_806Z-debug-0.log

To clarify, I did the following:

1. git clone https://github.com/moodmosaic/sbtc.git
2. cd sbtc/contracts
3. npm i
4. npx rv . sbtc-registry invariant

Am I doing something wrong?

[BowTiedRadone]

Quick question before starting debugging: did you checkout the rendezvous branch of moodmosaic/sbtc?

[BowTiedRadone]

@setzeus Checked on a clean VM–no globally installed rendezvous. The following steps worked on my end:

1. git clone https://github.com/moodmosaic/sbtc.git
2. cd sbtc/contracts/
3. git checkout rendezvous
4. npm i
5. npx rv . sbtc-registry invariant

Sample output:

[setzeus]

Hi hi @BowTiedRadone, tried the instructions above & got the following now:

setzeus@MacBookPro contracts % npx rv . sbtc-registry invariant
/Users/setzeus/Documents/github/sbtc-v2/jul-6-882-review/sbtc/contracts/node_modules/@stacks/rendezvous/node_modules/@hirosystems/clarinet-sdk-wasm/clarinet_sdk.js:1749
const wasmModule = new WebAssembly.Module(bytes);
                   ^

CompileError: WebAssembly.Module(): invalid value type 'externref', enable with --experimental-wasm-reftypes @+109
    at Object.<anonymous> (/Users/setzeus/Documents/github/sbtc-v2/jul-6-882-review/sbtc/contracts/node_modules/@stacks/rendezvous/node_modules/@hirosystems/clarinet-sdk-wasm/clarinet_sdk.js:1749:20)
    at Module._compile (node:internal/modules/cjs/loader:1198:14)
    at Object.Module._extensions..js (node:internal/modules/cjs/loader:1252:10)
    at Module.load (node:internal/modules/cjs/loader:1076:32)
    at Function.Module._load (node:internal/modules/cjs/loader:911:12)
    at Module.require (node:internal/modules/cjs/loader:1100:19)
    at require (node:internal/modules/cjs/helpers:119:18)
    at Object.<anonymous> (/Users/setzeus/Documents/github/sbtc-v2/jul-6-882-review/sbtc/contracts/node_modules/@stacks/rendezvous/node_modules/@hirosystems/clarinet-sdk/dist/cjs/node/src/index.js:38:29)
    at Module._compile (node:internal/modules/cjs/loader:1198:14)
    at Object.Module._extensions..js (node:internal/modules/cjs/loader:1252:10)

[BowTiedRadone]

@setzeus that's interesting. I just tried it on my MacBook and it's working fine for me. What's your setup like (Node version, etc.)? Also, here's the Rendezvous workflow file we run for all PRs and releases, and all the tests are passing on macOS in our CI. I'm thinking this might be a versioning issue.

[moodmosaic]

I'm thinking this might be a versioning issue.

In order to say, @setzeus can you let us know your environment please? /cc @hugocaillard

[BowTiedRadone]

@setzeus Any updates on this?