Skip to content

Commit 443f5a9

Browse files
committed
Update README with Kani proofs
Update README with existing Kani proofs. Signed-off-by: Matias Ezequiel Vara Larsen <[email protected]>
1 parent 9d26f93 commit 443f5a9

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

README.md

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -107,6 +107,15 @@ need to unblock the pipeline by following the Buildkite run link in the PR and
107107
click on the corresponding
108108
[unblock pipeline button](https://buildkite.com/docs/pipelines/block-step).
109109

110+
## Kani proofs
111+
We run Kani proofs for each PR and on merges to the main branch. The proofs
112+
check conformance of the virtio-queue implementation to requirements from the
113+
virtio specification. Different than a unit test, a proof is checked for every
114+
possible input thus enforcing conformance. This is a list of the existing
115+
conformance proofs:
116+
117+
* Conformance to 2.7.7.2 section
118+
110119
## License
111120

112121
This project is licensed under either of

0 commit comments

Comments
 (0)