Awesome-halmos

February 7, 2025 · View on GitHub

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

halmos

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