Tool Integrations

[michalsustr]

I came across this project and it looks very interesting. For now, it looks like you are doing just the specification, or is there an existing integration with some verification tools (e.g. what you list in README)?

Thank you.

[mkovaxx]

@michalsustr Thanks for adding a question!

Tool integrations are in the planning phase.

The following ideas seem most immediately actionable:

• cargo-fuzz: Build a tool (e.g. anodized-fuzz) that generates fuzz_target!s based on specs.
• Kani: Build a tool or new runtime behavior that targets Kani, piggybacking on its ability to prove the absence of panic!s.
• Charon: Find a way to expose specs through Charon, so that verifiers that use it (e.g. Aeneas) have access to them.

Do any of those seem relevant to your use cases?

Can you think of other directions we should explore?

[tv42]

Verus's biggest annoyance for this mere-programmer is that everything has to written inside the verus! macro, ruining the developer experience. My biggest hope is that someone can convince the people working on formal methods for Rust actually consider Rust and not their mathematical conventions as the starting point (I'm looking at you Creusot).

Kani is quite pleasant-looking, but quite limited in its approach, e.g. loops are very hard to handle with it. Fuzzing is great. But, in those contexts (proving panic-freeness), it's a little dubious what benefit there is in writing #[spec(requires)] instead of fn foo() { assert!(...) }.

Anodized seems great but if it's just in a vacuum with no formal tooling that understands its conventions, it seems too early to get excited about.