Specify. (Code.) Verify.
The rules of software development are changing. AI agents generate code faster than humans can review it. AI auditors uncover critical vulnerabilities that must be quickly patched before attackers exploit them.
At pereq, we craft tools that help developers bring rigorous specification and verification into their workflows, so they can rapidly build new software and evolve existing systems with confidence in their correctness and security.
Products
-
hax
An open-source toolchain that helps developers verify their Rust code for correctness and security using proof frameworks like Lean, F*, and ProVerif.
-
perspec
An automated tool suite that dovetails with AI agents to help developers write rigorous specifications and verify the correctness and security of their code. Coming soon.
Proven in practice. Grounded in research.
Our tools build on the latest advances in formal verification and security analysis and are shaped by the demands of real-world software. They are continuously tested and improved through collaborations with companies such as Google, Signal, Nym, and SandboxAQ.
Explore pereq.dev for our tools, documentation, and research.
Who we are
We believe that formal rigor and creativity go hand in hand. We take inspiration from Georges Perec and the Oulipo group, who showed how mathematical constraints can open up new possibilities, producing works that are surprising and delightful.
Software works the same way. Well-crafted specifications and formal proofs do not merely stop programs from misbehaving. They give developers the freedom to innovate with confidence.
News and events
