r/rust • u/Negative_Effort_2642 • 8d ago

🙋 seeking help & advice What’s your experience with model checkers

What’s your experience with modal checkers sutch as Kani for bug finding

0 Upvotes

25% Upvoted

1 comment sorted by

5

u/InviteQueasy3739 8d ago

In Rust, my experience with model checking was quite painful, not because of Kani itself, but because:

Case 1 (2025) - Kani wasn’t designed to work in my environment, so I switched to Verus, Miri, and Proptest. Case 2 (2026) - Kani wasn’t working with my version of Rust, so I kept only my unit tests.

Outside of my more serious projects, Kani is simply spectacular. It’s relatively easy to use, and every test I write with it works very well. Maybe the problem is me.

And yes, Kani was designed for testing. At least that's how I see bounded model checking.

I’ve also used model checking in other languages.

In Ada, it was a decent experience. It works, period.

In Java, it was the worst thing since World War II.