Formal verification / property testing

[ChristopherRabotin]

1. What should be formally verified?
2. How should it be verified?

References:

• https://github.com/project-oak/rust-verification-tools
• https://github.com/AltSysrq/proptest
• https://github.com/BurntSushi/quickcheck/ (and differences between quickcheck and proptest here)

[ChristopherRabotin]

After having tested out the Hypothesis package in Python, it seems pretty evident that this would be extremely important for hardening the code and execution flow.

Relevant resources:

• https://rust-fuzz.github.io/book/afl/tutorial.html
• https://blog.trailofbits.com/2019/11/11/test-case-reduction/
• https://github.com/AltSysrq/proptest

[ChristopherRabotin]

Kani is a really clever formal verification tool that I've now successfully used on hifitime. It doesn't rely on random generation of test cases like Hypothesis and prop_test.