We automate most of our formatting preferences. Our CI will run format checkers for PRs and pushes. These checks are required for merging any PR.
For Rust, we use rustfmt
which is configured via the rustfmt.toml file.
We are also in the process of enabling
Because of that, we still have a couple of lints disabled (see .cargo/config for the updated list).
We recognize that in some cases, the formatting and lints automation may not be applicable to a specific code.
In those cases, we usually prefer explicitly allowing exceptions by locally disabling the check.
#[allow] annotation instead of disabling a link on a crate or project level.
All source code files begin with a copyright and license notice. If this is a new file, please add the following notice:
// Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT
When modifying a file from another project, please keep their headers as is and append the following notice after them:
// ... existing licensing headers ... // Modifications Copyright Kani Contributors // See GitHub history for details.
Note: The comment escape characters will depend on the type of file you are working with. E.g.: For rust start the
//, but for python start with
We also have automated checks for the copyright notice. There are a few file types where this rule doesn't apply. You can see that list in the copyright-exclude file.
We are developing Kani to provide assurance that critical Rust components are verifiably free of certain classes of security and correctness issues. Thus, it is critical that we provide a verification tool that is sound. For the class of errors that Kani can verify, we should not produce a "No Error" result if there was in fact an error in the code being verified, i.e., it has no "False Negatives".
Because of that, we bias on the side of correctness. Any incorrect modeling that may trigger an unsound analysis that cannot be fixed in the short term should be mitigated. Here are a few ways how we do that.
Make sure to add user-friendly errors for constructs that we can't handle. For example, Kani cannot handle the panic unwind strategy, and it will fail compilation if the crate uses this configuration.
In general, it's preferred that error messages follow these guidelines used for
If the errors are being emitted from
kani-compiler, you should use the compiler error message utilities (e.g., the
Session::span_err method). However, if the
errors are being emitted from
kani-driver, you should use the functions provided in the
util module in
Even though this doesn't provide users the best experience, you are encouraged to add checks in the compiler for any
assumptions you make during development.
Those checks can be on the form of
Please provide a meaningful message to help user understand why something failed, and try to explain, at least with
a comment, why this is the case.
We don't formally use any specific formal representation of function contract, but whenever possible we do instrument the code with assertions that may represent the function pre- and post-conditions to ensure we are modeling the user code correctly.
In cases where Kani fails to model a certain instruction or local construct that doesn't have a global effect,
we encode this failure as a verification error.
I.e., we generate an assertion failure instead of the construct we are modeling using
which blocks the execution whenever this construct is reached.
This will allow users to verify their crate successfully as long as
that construct is not reachable in any harness. If a harness has at least one possible execution path that reaches
such construct, Kani will fail the verification, and it will mark all checks, other than failed checks, with
It is OK to add "TODO" comments as long as they don't compromise user experience or the tool correctness. When doing so, please create an issue that captures the task. Add details about the task at hand including any impact to the user. Finally, add the link to the issue that captures the "TODO" task as part of your comment.
// TODO: This function assumes type cannot be ZST. Check if that's always the case. // https://github.com/model-checking/kani/issues/XXXX assert!(!typ.is_zst(), "Unexpected ZST type");
We aim at writing code that is performant but also readable and easy to maintain. Avoid compromising the code quality if the performance gain is not significant.
Here are few tips that can help the readability of your code:
- Sort match arms, enum variants, and struct fields alphabetically.
- Prefer concise but meaningful names.
- Prefer exhaustive matches.
- Prefer declarative over imperative programming.