Symbolic Execution (Halmos)
Relevant source files
The following files were used as context for generating this wiki page:
Symbolic execution in Canon Guard is implemented using Halmos, a formal verification tool for Ethereum smart contracts. It serves as a complementary verification layer alongside unit tests, integration tests, and Medusa-based fuzzing to ensure the security and correctness of the multisig solution's on-chain Actions and timelock mechanisms.
Sources: CLAUDE.md:76-80, README.md:65-67
Within the project's testing hierarchy, symbolic execution provides a mathematically rigorous method to prove that contract properties hold across all possible execution paths. This is particularly critical for the core architecture, including the SafeEntrypoint, ActionHub, and various Action Builders that manage time-delayed transaction execution.
Sources: CLAUDE.md:11-17, CLAUDE.md:81
Integration and Configuration
Halmos is integrated into the project's development workflow through defined scripts and dependencies. The environment utilizes specialized cheatcodes to facilitate symbolic reasoning within the Foundry-based ecosystem.
Dependencies and Remappings
The project includes specific dependencies to support Halmos operations, mapping them for use within Solidity test files.
| Dependency | Purpose |
|---|---|
halmos-cheatcodes | Provides cheatcodes for symbolic execution and formal verification |
forge-std | Standard library used in conjunction with Halmos for testing |
Sources: package.json:62-63, remappings.txt:1-2
Execution Workflow
Developers trigger symbolic execution via the project's task runner. The process requires Halmos to be installed on the local machine.
yarn test:symbolic
Sources: package.json:34, README.md:65-67
The following diagram illustrates how Symbolic Execution fits into the broader testing and verification pipeline of the Canon Guard repository:
The diagram shows the parallel testing paths where Halmos provides formal proofs that complement functional and probabilistic testing methods.
Sources: CLAUDE.md:76-81, README.md:46-67
Verification Scope
Symbolic execution is used to verify the same core security properties and invariants defined for the system's safety. While invariant testing (fuzzing) explores these properties through random inputs, Halmos attempts to prove them.
Key Verification Targets
Based on the project's security properties, symbolic execution focuses on:
- Cap & Accounting: Proving that cap limits can never be exceeded regardless of epoch boundaries.
- Transaction Timing: Verifying that
expiresAt > executableAtandexecutableAt >= queuedAtfor all possible states. - Approval Logic: Ensuring that transactions only exist for approved action builders or hubs.
- Queue Integrity: Mathematically confirming that the queue remains free of duplicates and in sync with transaction mappings.
Sources: test/invariants/PROPERTIES.md:11-40
Logic Flow for Time-Delayed Transactions
Halmos is used to verify the logic within SafeEntrypoint regarding transaction delays.
The sequence diagram demonstrates the logical verification of the timelock mechanism, ensuring execution is impossible before the defined delay.
Sources: CLAUDE.md:12-17, test/invariants/PROPERTIES.md:47-55
Comparison with Fuzzing
While the repository uses Medusa for invariant fuzzing, Halmos provides a different level of assurance.
| Feature | Medusa (Fuzzing) | Halmos (Symbolic) |
|---|---|---|
| Method | Random Input Generation | Mathematical Proof |
| Coverage | Probabilistic | Exhaustive (within bounds) |
| Setup File | medusa.json | halmos command |
| Primary Goal | Find counter-examples | Prove properties |
Sources: medusa.json:1-10, package.json:32-34, README.md:61-67
Summary
Symbolic execution via Halmos is a critical component of the Canon Guard security stack. By moving beyond functional testing into formal verification, the project ensures that high-stakes multisig operations—such as dynamic timelocks and on-chain Actions—behave correctly under all possible mathematical conditions. It works in tandem with the Foundry-based build system and Medusa fuzzer to provide a comprehensive defense-in-depth strategy for the smart contract suite.
Sources: CLAUDE.md:1-20, README.md:1-10