In the tutorial here [1] they first setup the property based test and it doesn't find panic, but then they setup proof harness and this finds the panic immediately, so my question is what exactly happens under the hood? I read it uses some SAT solver, but the details are unclear in the docs. Thanks.
You might find this blog post helpful:
The key part is:
Internally, this verification process is a bit more complicated, and can be split into three main stages:
- Compilation: The Rust crate under verification and its dependencies are compiled into a program in a format that’s more suitable to verification.
- Symbolic execution: This program is then symbolically executed in order to generate a single logic formula that represents all possible execution paths and the properties to be checked.
- Satisfiability solving: This logic formula is then solved by employing a SAT or SMT solver that either finds a combination of concrete values that can satisfy the formula (a counterexample to a property exists), or prove that no assignment can satisfy the formula (all properties hold).
In fact, Kani employs a collection of tools to perform the different stages of the verification. Kani’s main process is called
kani-driver, and its main purpose is to orchestrate the execution and communication of these other tools:
- The compilation stage is done mostly1 by
kani-compiler, which is an extension of the Rust compiler that we have developed.kani-compilerwill generate agoto-programby combining all the code reachable from a harness.- For the symbolic execution stage, Kani invokes CBMC.
- The satisfiability checking stage is performed by CBMC itself, by invoking a satisfiability (SAT) solver such as MiniSat.
2 Likes
This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.