A curated list of resources on halmos, featuring blogs, videos, code repositories, and practical examples.
- Github: halmos.
- Telegram chat: halmos Telegram.
- halmos Getting Started: Beginner guide to understand how halmos works.
- halmos FAQ: answers to the most frequently asked questions.
- Invariant Testing with halmos by Antonio Viggiano: From invariant testing to Formal verification.
- Leveraging Existing Tests by a16z: How to level-up your existing tests with symbolic execution.
- @zachobront X Thread: Solady FixedPointMathLib Testing: Solady and Solmate equivalence check.
- @daejunpark X Thread: My halmos usage #1: using halmos for equivalence check.
- @0xkarmacoma X Thread: Solving CurtaCTF with halmos: How karmacoma used halmos for solving a curtaCTF.
- Halmos vs Damn Vulnerable Defi: A series of writeups on solving Damn Vunerable DeFi CTF with Halmos.
- Beyond Fuzzing Symbolic Testing in Practice by karmacoma: Understanding path exploration.
- From Fuzz to Symbolic Tests by Patrick Collins: A video tutorial on transitioning from fuzz to symbolic testing.
- Path Explosion and Timeout by Cyfrin: Understanding path explosion and timeouts.
- Setting First Test with halmos by Cyfrin: A video tutorial on setting up your first halmos test.
- Testing WSL with halmos by Cyfrin: A video guide on testing WSL function.
- halmos-sandbox: A repository with +90 halmos test examples.
- halmos-solady: Examples of halmos tests for the Solady library.
- ERC20 Symbolic Tests: Symbolic tests for Solady, Solmate, and OpenZeppelin ERC20 tokens.
- ERC721 Symbolic Tests: Symbolic tests for Solady, Solmate, and OpenZeppelin ERC721 tokens.
- WETH Symbolic Testing by horsefacts: Symbolic testing for WETH9 contract.
- Property-Based Testing Benchmark by Antonio Viggiano: Benchmarks for property-based testing.
- DEI Stablecoin Symbolic Test: Symbolic tests for the DEI Stablecoin.
- Curve Token V3 Symbolic Test: Symbolic tests for Curve Token V3.
- SignatureChecker Equivalence Check: Equivalence check between OpenZeppelin and Solady's SignatureChecker.
- ERC20 Differential Tests by Antonio Viggiano: Halmos Differential Tests for OpenZeppelin, Solady, and Solmate ERC-20 Token Implementations.
- Morpho: Symbolic tests for Morpho's data structures.
- Cicada: Verifying Cicada's big number arithmetic library with symbolic tests.
- LibPrimeTest: Symbolic tests for prime number library.
- LibUint1024Test: Symbolic tests for 1024-bit unsigned integer library.
- Farcaster: Verifying Farcaster's onchain registry contracts.
- IdRegistrySymTest: Symbolic tests for IdRegistry.
- KeyRegistrySymTest: Symbolic tests for KeyRegistry.
- snekmate: Symbolic tests for Vyper-based
erc20,erc721,erc1155, andmathcontracts. - Pimlico: Symbolic tests for ERC20Paymaster