Hacker News Reader

> Production-ready by formal verification, model checking, deterministic simulation, fuzzing, and lots of testing.

What does model checking mean here?

My guess is https://en.wikipedia.org/wiki/Model_checking . C Bounded Model Checker [0] is a relatively well-known instance in the niche.

[0]: https://www.cprover.org/cbmc/

No, he used verus, a rust tool. And shuffle and ffs. See his docs

Sure. I didn't mean to say that the author used CBMC, only that it's an example of model checking.

Incidentally, the docs don't seem to say what model checker was used. I don't think any of verus, shuffle, or ffs are technically model checkers (or at the very least they don't describe themselves as such)

Thanks. This is helpful.

Reply on news.ycombinator.com