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
- Formally Verifying the Easy Partbrainflow.substack.com
- The Compute Verification Postfirstscattering.com
- Automatic Formal Verification for Code Generationlogicalintelligence.com
- AI Will Write All the Code. Mathematics Will Prove It Works.menlovc.com
- Formalizing Fermat's Last Theoremanthropic.com
- Verifying smart contracts | ethereum.orgethereum.org
- Formally Verifying WebAssembly - A Soroban Case Studycertora.com
- lf-lean: The frontier of verified software engineering | Theoremtheorem.dev
- The Compute Verification Postsubstack.com
- Auto-review of agent actions without synchronous human oversightalignment.openai.com