Coding conventions

Formatting

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 clippy. Because of that, we still have a couple of lints disabled (see .cargo/config for the updated list).

We also have a bit of C and Python code in our repository. For C we use clang-format and for Python scripts we use autopep8. See .clang-format and pyproject.toml for their configuration.

Exceptions

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. E.g., use #[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 header with //, 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.

Code for soundness

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.

Compilation errors

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 rustc development. 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 kani-driver.

Internal compiler errors

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 assert!() or unreachable!() statement. 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.

Verification errors

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 codegen_unimplemented(), 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 UNDETERMINED status.

Create detailed issues for "TODO" tasks

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.

E.g.:

// 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");

Performant but readable

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.