Klever is a static verification framework that aims at automated checking of programs developed in the C programming language against a variety of correctness rules using tools implementing such methods of thorough static analysis as Bounded Model Checking and Counterexample-Guided Abstraction Refinement.

The current version of Klever allows to find memory safety issues, e.g. buffer over-reads/writes and null pointer dereferences, data races and incorrect usages of the most popular Linux kernel API as well as to prove formal correctness under certain assumptions for Linux kernel loadable modules. We have implemented specifications for modeling interrupts, timers and interfaces of kernel subsystems including USB, PCI, SCSI, SERIAL, NET, file systems, etc. Klever 2.0 will complete support of automated static verification for other C software.

As static verification back-ends Klever supports CPAchecker and Ultimate Automizer. Moreover, one can integrate other tools participated in the competition on software verification.

For starting static verification and for comprehensive analysis of results Klever provides a multiuser web graphical interface. It shows both details, e.g. error traces that contain all statements and possible values of variables and function arguments from a program start to a found error, and statistics like the total number of bugs and false alarms. Experts can create marks associating automatically with all similar results.

If you have any questions, feel free to send an email to .

Klever online documentation:

Klever Gitter chat:

List of bugs found in the Linux kernel and acknowledged by the developers:

Issue tracking

open closed Total
Bug 128 430 558
Feature 245 485 730

View all issues