Sequent — software you can trust
Sequent builds Alan, a prover agent for deep formal verification of smart contracts: machine-checked, unbounded, replayable proofs. Don't trust us. Re-run it.
The state of the art Contracts holding real value ship on evidence that goes stale the moment the code changes, or evidence that only covers the cases somebody thought to try. An audit is a snapshot A manual audit is expert opinion about one version of the code, delivered weeks later as a PDF. The code keeps changing after the reviewers leave, and the review covered the cases they thought to check. Bounded checkers stop at depth k Bounded model checking unrolls your contract to a finite depth and reports that no counterexample exists within that bound. Unbounded loops and unbounded…
saved by
related reading
- A shallow dive into formal verificationvitalik.eth.limo
- When AI Writes the World's Software, Who Verifies It? — Leonardo de Mouraleodemoura.github.io
- Quint: executable specifications for reliable systemsquint.sh
- Why We Built Our Own Background Agentbuilders.ramp.com
- AI Will Write All the Code. Mathematics Will Prove It Works.menlovc.com
- Automatic Formal Verification for Code Generationlogicalintelligence.com
- Formally Verifying the Easy Partbrainflow.substack.com
- The Compute Verification Postfirstscattering.com
- Sequent: Scale and Automation for Higher Confidence in Alignment — Sequentsequent.org
- Advanced AI Workflow Automation Software & Tools - n8nn8n.io
- lf-lean: The frontier of verified software engineering | Theoremtheorem.dev
- On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications | Proofs and Intuitionsproofsandintuitions.net