Hacker GitHub

← All repos

model-checking/kani

View on GitHub ↗ ★ 3,628 Rust

A model checker for Rust programs.

18 mentions on Hacker News by 15 people: 2 stories, 16 comments · first 2022-03-26 · latest 2026-09-17

Mentions per year 18 mentions · busiest year 2024 (6)
20082026
AllStoriesComments NewestTopOldest
  1. …them so I'll refrain from trying to differentiate them. [0] https://github.com/rust-lang/miri [1] https://github.com/model-checking/kani [2] https://github.com/creusot-rs/creusot
    comment by 63 · 2026-09-17 · in Developing provably correct Rust code with Verus
  2. …source code. A couple of examples, in a rough order of approachability by a working programmer: https://github.com/model-checking/kani https://github.com/flux-rs/flux https://github.com/viperproject/prusti-dev https://creusot.rs/ I really…
    comment by yencabulator · 2026-08-17 · in The Case Against Formal Verification, 50 Years Later
  3. …converts the Rust code and C code into a GOTO program[1] which verifiers can then run on top of [0] https://github.com/model-checking/kani [1] https://model-checking.github.io/cbmc-training/cbmc/overview...
    comment by malisper · 2026-07-30 · in Why don't people use formal methods? (2019)
  4. …If you want to check out what all the verification look like, you can see them here[1] [0] https://github.com/model-checking/kani [1] https://github.com/malisper/pgrust/tree/main/proofs
    comment by malisper · 2026-07-30 · in Why don't people use formal methods? (2019)
  5. …), as long as you don't accidentally need e.g. randomness for HashMap DoS protection ( https://github.com/model-checking/kani/issues/2423#issuecomm... ). Loops are an utter pain to prove with Kani, though:…
    comment by yencabulator · 2025-06-03 · in What works (and doesn't) selling formal methods
  6. …All in all, it seems to me like Rust supports a wide variety of use cases pretty nicely. [0]: https://github.com/model-checking/kani
    comment by genrilz · 2025-05-07 · in Matt Godbolt sold me on Rust by showing me C++
  7. I researched and discovered kani https://github.com/model-checking/kani , it's pretty cool. ```rust #[kani::proof] fn main() { let mut array: [i32; 10] = kani::any(); array.sort_unstable(); let index: usize = kani::any_where(|i| *i > 0 &&…
    comment by koakuma-chan · 2025-04-13 · in Rust to C compiler – 95.9% test pass rate, odd platforms
  8. …but some context: > I'm not aware of one for rust, but there is a lot of progress in this area https://github.com/model-checking/kani is probably the best known one, I believe there are a few others. > (I'm not sure what rust allows,…
    comment by steveklabnik · 2025-01-23 · in Isolating complexity is the essence of successful abstractions
  9. does Kani count? https://github.com/model-checking/kani
    comment by drdrey · 2024-08-27 · in KLEE Symbolic Execution Engine
  10. …subset of Rust. If that manages to get to you all the way to the end result, then there was no gap. https://github.com/model-checking/kani http://prusti.org/
    comment by yencabulator · 2024-06-24 · in Formal methods: Just good engineering practice?
  11. Is there any relationship between this and Kani[1]? Do they work differently? [1] https://github.com/model-checking/kani
    comment by TachyonicBytes · 2024-05-04 · in Verified Rust for low-level systems code
  12. …is far from the speed and robustness of the C front end. [1] https://github.com/diffblue/cbmc [2] https://github.com/model-checking/kani
    comment by animatethrow · 2024-03-28 · in Xr0 Makes C Safer than Rust
  13. This is also the backend for Kani - Amazon's formal verification tool for Rust. https://github.com/model-checking/kani
    comment by IshKebab · 2024-01-30 · in The C bounded model checker: criminally underused
  14. …seems like the best route. I feel like Rust leans into this paradigm with `unsafe` blocks. [1] - https://github.com/model-checking/kani
    comment by bennettnate5 · 2023-09-12 · in Chrome: Heap buffer overflow in WebP
  15. …search space if possible. [0]: https://medium.com/@carlmkadie/check-ai-generated-code-perfe... [1]: https://github.com/model-checking/kani
    comment by rocho · 2023-06-15 · in This Week in Rust 499
  16. …to this. Various sources point to rmc as https://github.com/model-checking/rmc (redirected to https://github.com/model-checking/kani ) and https://model-checking.github.io/rmc/ (404). Anyone knows why?
    comment by euske · 2022-03-26 · in Kani Rust Verifier – a bit-precise model-checker for Rust