kani-stylus

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.