Examples

This chapter contains various examples that demonstrates how hax can be used to prove properties about programs. Each example is self-contained. hax being a tool that can extract Rust to various backends, this section provides examples for each backend.

The first subsection takes some examples from Rust by Example, and shows how to prove properties on them.

The other sections present backend-specific examples.