From eec5968ddc0521b265b6dc0d198682d6c05718cb Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 14 Feb 2023 18:52:04 -0800 Subject: [PATCH] Tune down recommendation and point to bolero --- docs/src/application.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/docs/src/application.md b/docs/src/application.md index e41b75050549..fb527679e2c6 100644 --- a/docs/src/application.md +++ b/docs/src/application.md @@ -6,9 +6,8 @@ You may be interested in applying Kani if you're in this situation: 2. You've already invested heavily in testing to ensure correctness. 3. You want to invest further, to gain a much higher degree of assurance. -> If you haven't already, we recommend techniques like property testing (e.g. with [`proptest`](https://github.com/AltSysrq/proptest)) before attempting model checking. -> These yield good results, are very cheap to apply, and are often easier to adopt and debug. -> Kani is a next step: a tool that can be applied once cheaper tactics are no longer yielding results, or once the easier to detect issues have already been dealt with. +> If you haven't already, we also recommend techniques like property testing and fuzzing (e.g. with [`bolero`](https://github.com/camshaft/bolero/)). +> These yield good results, are very cheap to apply, and are often easy to adopt and debug. In this section, we explain [how Kani compares with other tools](./tool-comparison.md) and suggest [where to start applying Kani in real code](./tutorial-real-code.md).