Invslicer
Invslicer is an open-source tool by Invariant Labs for extracting invariant-critical code slices from smart contracts.
prove the invariant. ship the protocol.
A research-driven security firm that leverages formal methods for smart contracts, blockchains, zero-knowledge circuits, and adversarial protocols.
Tools
Services
formal verification
We design custom formal verification workflows for blockchains, smart contracts, and protocol-critical systems. Our work centers on defining security properties, modeling protocol assumptions, and proving that implementation behavior preserves the invariants the system depends on.
Research
Last Whisper: From Provenance Chain Halt to Infinite Mint
A boundary failure in Provenance marker creation flows that turned metadata scope denoms into an Infinite Mint primitive and deterministic chain halt.
An Introduction to Formal Verification: From Sorting Algorithms to Finding a Vulnerability with Dafny
A practical Dafny walkthrough from proving Bubble Sort, Quick Sort, and Merge Sort to finding a vulnerability in stage-accounting.
An Introduction to Formal Verification: Proving Your First Program
A first-principles walkthrough of SMT, program annotations, basic paths, weakest preconditions, and verification conditions.
Contact
Building a protocol where failure is expensive? Send the threat model, codebase, and properties you believe should hold under every adversarial execution.