Awesome-halmos

A curated list of resources on halmos, featuring blogs, videos, code repositories, and practical examples.

halmos

• Github: halmos.
• Telegram chat: halmos Telegram.

halmos Knowledge base

• 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.

Videos

• 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.

Test Examples

• 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.

Projects Using halmos

• 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, and math contracts.
• Pimlico: Symbolic tests for ERC20Paymaster