Current tooling for testing and verification on Soroban / Stellar

[dkcumming]

Here are some methods and tools used for testing and / or verification of Soroban / Stellar smart contracts

cargo test

• Able to deploy contracts and manipulate the state (funding addresses with currencies, etc.)
• Good for unit testing
• Good for fuzzing with proptest
• Unable to test some behaviours of Soroban (storage entries extending past ttl for example)
• Unable to test with an established blockchain context, such as the current state of the testnet
• examples: ex1, ex2

testnet deployment

• Deploying the contract to the Soroban Testnet
• Interface through Soroban CLI
• Good for testing how the contract will actually behave on the Testnet
• Blocktime is slow, so not a good place for testing boundaries of TTL etc.
• Can view blocks on Stellar Chain Explorer and Stellar Expert
• Somewhat clunky, but precise

Docker quickstart instance deployment

• Docker image to run the Stellar network
• Github, Guide1, Guide2
• Can deploy to pubnet (mainnet?), testnet, futurenet, local
• Can override parameters to customize things (like blocktime) to observe behaviours that are otherwise unpractical to observe

Okashi

• okashi.dev
• Playground to deploy a Soroban contract, and interact with the external functions through a GUI with a view to low level data
• Can view WASM (no source mapping)
• Can view Storage
• Can view Console for log of transactions
• Able to deploy to Okashi (local testnet), Futurenet (Updated Testnet?), Testnet, Mainnet

Flux

• Adds refinement types to Rust
• Github, website
• Won't work out-of-the-box, required modifications to Soroban sdk to work in demo
• z3 in association with Rust type system determines that predicates hold
• Tried to install and get working by copying the changes in the demo, but I could not get this tool to run

Galois Formal Verso

• Verifier for Soroban contracts
• Github, Demo
• Only supports Soroban SDK v0.8.4
• Many steps to install, after a lot of frustration trying to get the install to work I gave up

Certora Verifier (Under Construction)

• Verifier of WASM
• Decompiles .wat file into secret Certora Prover IR TAC which then generates verification conditions that are sent to an SMT (z3, cvc5, etc.).
• Blackbox as internals are closed source
• UI seems a little clunky in the demo
• Using the tool requires a sign up, I didn't sign up so haven't tried it

Scout

• Static analysis tool for Stellar Soroban
• Github, docs
• This tool was super easy to install, and also has a VsCode extension "Scout Audit"
• The only FM tool for Soroban that I have tried that installed and worked
• Tried on the FxDAO code base and it was great, a bunch of stuff identified wasn't actually a problem (still good to have notified), and 2 things were great to have pointed out that I hadn't considered and could indeed be an issue potentially.

Miscellaneous

xycLoans

• Flash Loans on Stellar-Soroban
• Github, website

Slender

• Lending platform that is intending to implement Flash Loans

Couldn't Find

I was hoping to find something like the echinda fuzzer for Solidity, but it appears nothing like that currently exists for Soroban