Current tooling for testing and verification on Soroban / Stellar

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

No repository files, tests, or entry points are named. Start by defining the documentation scope for this tooling survey, then verify the listed Soroban and Stellar tools, links, capabilities, and limitations. Done means producing an agreed, current guide that covers the relevant testing and verification options.