← Back to ResearchExplainerExplainerExplainerExplainerExplainer
Explainers
Plain-language introductions to formal verification concepts.
When to Verify Bytecode Instead of Solidity
Why formal verification should usually model Solidity directly, and why the EIP-8282 builder predeploys were the exception.
From Foundry Invariants to Lean Proofs
Bridging Foundry invariant testing and formal verification with Lean.
ERC-4337 EntryPoint Execution Invariant
A reproducible two-mode scenario for one modeled EntryPoint v0.9 handleOps execution-count invariant.
Proving the SPHINCS- Post-Quantum Verifiers
A hand-held tour of SPHINCS-, what a correct on-chain verifier must check, and how we proved it in Lean 4 with Verity.
What is a formal proof?
A short explanation for non-specialists.