Products

Documentation and playgrounds for pereq's verification tools.

hax

An open-source toolchain that helps developers verify their Rust code for correctness and security using proof frameworks like Lean, F*, and ProVerif.

cargo hax into lean

Quick start

PlaygroundRun hax in your browser.
ManualTutorials for using hax to verify Rust code with Lean and F*.
GitHubSource code, issues, and contributions.
ZulipQuestions and discussion.

Coming soon

perspec

Specification-driven development with AI and formal methods.

About perspec

Research

Our tools build on research in formal verification, programming languages, and software security.

Explore our publications and talks