Developer tools
Documentation and playgrounds for pereq's verification tools.
hax
Translate a large subset of Rust into Lean, F* or Rocq, and prove that your code does what it should.
cargo hax into lean- Quick startInstall hax and extract your first crate.
- ManualTutorials for Lean and F*, tool versions, FAQ.
- PlaygroundRun hax in the browser and share the result.
- Dev blogRelease notes and monthly updates.
- GitHubSource, issues and contributions.
- ZulipQuestions and discussion.
Coming soon
perspec
Specification-driven development for the age of AI coding agents. Documentation and a playground will appear here.