kani

Kani Rust Verifier (by model-checking)

Kani Alternatives

Similar projects and alternatives to kani

  1. rust

    2,831 kani VS rust

    Empowering everyone to build reliable and efficient software.

  2. InfluxDB

    InfluxDB – Built for High-Performance Time Series Workloads. InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.

    InfluxDB logo
  3. rfcs

    689 kani VS rfcs

    RFCs for changes to Rust

  4. bevy

    594 kani VS bevy

    A refreshingly simple data-driven game engine built in Rust

  5. FFmpeg

    497 kani VS FFmpeg

    Mirror of https://git.ffmpeg.org/ffmpeg.git

  6. Signal-Desktop

    325 kani VS Signal-Desktop

    A private messenger for Windows, macOS, and Linux.

  7. too-many-lists

    Learn Rust by writing Entirely Too Many linked lists

  8. yew

    208 kani VS yew

    Rust / Wasm framework for creating reliable and efficient web applications

  9. SaaSHub

    SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

    SaaSHub logo
  10. dmd

    155 kani VS dmd

    dmd D Programming Language compiler

  11. wasmer

    142 kani VS wasmer

    🚀 Fast, secure, lightweight containers based on WebAssembly

  12. miri

    124 kani VS miri

    An interpreter for Rust's mid-level intermediate representation

  13. rust-playground

    The Rust Playground

  14. nomicon

    89 kani VS nomicon

    The Dark Arts of Advanced and Unsafe Rust Programming

  15. validator

    75 kani VS validator

    :100:Go Struct and Field validation, including Cross Field, Cross Struct, Map, Slice and Array diving

  16. prusti-dev

    23 kani VS prusti-dev

    A static verifier for Rust, based on the Viper verification infrastructure.

  17. ring

    28 kani VS ring

    An experiment. (by briansmith)

  18. jxl.js

    25 kani VS jxl.js

    JPEG XL decoder in JavaScript using WebAssembly (WASM)

  19. rustig

    9 kani VS rustig

    A tool to detect code paths leading to Rust's panic handler

  20. MIRAI

    9 kani VS MIRAI

    Discontinued Rust mid-level IR Abstract Interpreter

  21. libwebp

    13 kani VS libwebp

    Mirror only. Please do not send pull requests. See https://chromium.googlesource.com/webm/libwebp/+/HEAD/CONTRIBUTING.md.

  22. s2n-quic

    8 kani VS s2n-quic

    An implementation of the IETF QUIC protocol

  23. SaaSHub

    SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

    SaaSHub logo
NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a better kani alternative or higher similarity.

kani discussion

Log in or Post with

kani reviews and mentions

Posts with mentions or reviews of kani. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2025-05-06.
  • Matt Godbolt sold me on Rust (by showing me C++)
    14 projects | news.ycombinator.com | 6 May 2025
    The point I'm sure was to prevent the checks from incurring runtime overhead in production. Even in release mode, the overflow will only wrap rather than trigger undefined behavior, so this won't cause memory corruption unless you are writing unsafe code that ignores the possibility of overflow.

    The checks being on in the debug config means your tests and replications of bug reports will catch overflow if they occur. If you are working on some sensitive application where you can't afford logic bugs from overflows but can afford panics/crashes, you can just turn on checks in release mode.

    If you are working on a library which is meant to do something sensible on overflow, you can use the wide variety of member functions such as 'wrapping_add' or 'checked_add' to control what happens on overflow regardless of build configuration.

    Finally, if your application can't afford to have logic bugs from overflows and also can't panic, you can use kani [0] to prove that overflow never happens.

    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

  • Rust to C compiler – 95.9% test pass rate, odd platforms
    8 projects | news.ycombinator.com | 12 Apr 2025
    I researched and discovered kani https://github.com/model-checking/kani, it's pretty cool.

    ```rust

  • Automated reasoning and generative AI: Harness creativity with formal verifications
    2 projects | dev.to | 28 Jan 2025
    Modern software verification employs various approaches, each offering different trade-offs between ease of use and strength of guarantees. AWS contributes to the open source program verification tools used in the previous examples. Dafny and Kani represent two powerful approaches to program verification. Let's see how they work in practice before connecting the dots between automated reasoning and generative AI.
  • Isolating complexity is the essence of successful abstractions
    2 projects | news.ycombinator.com | 22 Jan 2025
    I agree with what you're saying, 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, particularly in unsafe).

    You can't "cast const away" in Rust, even in unsafe. That is, you can do it in unsafe, but it is always undefined behavior to do so. (I am speaking about &T and &mut T here, const T and mut T exist and you're allowed to cast between those, as they have no real aliasing requirements and are really just a lint.)

  • Rust is rolling off the Volvo assembly line
    3 projects | news.ycombinator.com | 7 Oct 2024
  • Re-fixing Servo's event-loop
    1 project | news.ycombinator.com | 14 Aug 2024
    There's a model checker that can directly verify Rust code, Kani https://model-checking.github.io/kani/ - I wonder if Servo could use it in this case?
  • Kani: A bit-precise model checker for Rust
    1 project | news.ycombinator.com | 13 Jun 2024
  • The C Bounded Model Checker: Criminally Underused
    7 projects | news.ycombinator.com | 30 Jan 2024
    This is also the backend for Kani - Amazon's formal verification tool for Rust.

    https://github.com/model-checking/kani

  • Boletín AWS Open Source, Christmas Edition
    9 projects | dev.to | 24 Dec 2023
  • The Wizardry Frontier
    2 projects | /r/rust | 10 Dec 2023
    Nice read! Rust has pushed, and will continue to push, the limits of practical, bare metal, memory safe languages. And it's interesting to think about what's next, maybe eventually there will be some form of practical theorem proving "for the masses". Lean 4 looks great and has potential, but it's still mostly a language for mathematicians. There has been some research on AI constructed proofs, which could be the best of both worlds because then the type checker can verify that the AI generated code/proof is indeed correct. Tools like Kani are also a step forward in program correctness.
  • A note from our sponsor - SaaSHub
    www.saashub.com | 23 May 2025
    SaaSHub helps you find the best software and product alternatives Learn more →

Stats

Basic kani repo stats
54
2,550
9.7
7 days ago

model-checking/kani is an open source project licensed under Apache License 2.0 which is an OSI approved license.

The primary programming language of kani is Rust.


Sponsored
InfluxDB – Built for High-Performance Time Series Workloads
InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.
www.influxdata.com

Did you know that Rust is
the 5th most popular programming language
based on number of references?