Bounded model checking for Stylus. Write symbolic tests for formal verification of your Stylus contracts.
Bounded model checking for Stylus smart contracts, using Kani.
Stylus lets you write smart contracts in Rust. Kani is a bounded model checker for Rust that proves properties over all inputs within a bound — and hands you a concrete counterexample when one fails. This project is about wiring the two together and more: give a Stylus contract a symbolic host environment, then prove things like "transfers conserve total supply" and "only the owner can call this" instead of testing them one input at a time.
We conceived the idea and started building just a couple of days before the buildathon.
