Skip to content

Commit 00c1aef

Browse files
dreliq9claude
dreliq9
and
claude
committed
Add CI workflow running all six verification tiers
Runs on every push to main and every pull request: - Tier 1-3: forge test (unit, fuzz, 1.28M-call stateful invariants) - Tier 4: Slither static analysis (fails on medium+ severity) - Tier 5: Halmos symbolic verification (4 proofs) Runs on manual dispatch or PR label `run-mutation`: - Tier 6: slither-mutate + custom driver (mutation score) Badge added to README header. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 96d3ce1 commit 00c1aef

2 files changed

Lines changed: 132 additions & 0 deletions

File tree

‎.github/workflows/verify.yml‎

Lines changed: 129 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,129 @@
1+
name: verify
2+
3+
on:
4+
push:
5+
branches: [main]
6+
pull_request:
7+
workflow_dispatch:
8+
9+
concurrency:
10+
group: verify-${{ github.ref }}
11+
cancel-in-progress: true
12+
13+
jobs:
14+
# ───────────────────────── Tiers 1-3 ──────────────────────────────
15+
# Unit tests, fuzz properties, and stateful invariants (1.28M calls).
16+
test:
17+
name: Unit · Fuzz · Invariants
18+
runs-on: ubuntu-latest
19+
steps:
20+
- uses: actions/checkout@v4
21+
with:
22+
submodules: recursive
23+
24+
- uses: foundry-rs/foundry-toolchain@v1
25+
with:
26+
version: stable
27+
28+
- name: Forge version
29+
run: forge --version
30+
31+
- name: Build
32+
run: forge build --sizes
33+
34+
- name: Unit and fuzz tests (52 tests + 2 fuzz × 256 runs)
35+
run: forge test --no-match-contract 'Headless(Invariant|Halmos)'
36+
37+
- name: Stateful invariants (10 invariants × 128k calls = 1.28M)
38+
run: forge test --match-contract HeadlessInvariant
39+
40+
# ────────────────────────── Tier 4 ────────────────────────────────
41+
# Slither static analysis. Fails on medium or higher severity.
42+
# Informational findings (low-level-calls) are expected and allowed.
43+
slither:
44+
name: Tier 4 · Slither static analysis
45+
runs-on: ubuntu-latest
46+
steps:
47+
- uses: actions/checkout@v4
48+
with:
49+
submodules: recursive
50+
51+
- uses: foundry-rs/foundry-toolchain@v1
52+
with:
53+
version: stable
54+
55+
- name: Slither
56+
uses: crytic/slither-action@v0.4.0
57+
with:
58+
target: '.'
59+
slither-args: --filter-paths "lib/" --exclude-informational --exclude-low
60+
fail-on: medium
61+
62+
# ────────────────────────── Tier 5 ────────────────────────────────
63+
# Halmos symbolic verification. Proves 4 load-bearing properties
64+
# across the full symbolic path space (bounded amounts).
65+
halmos:
66+
name: Tier 5 · Halmos symbolic verification
67+
runs-on: ubuntu-latest
68+
steps:
69+
- uses: actions/checkout@v4
70+
with:
71+
submodules: recursive
72+
73+
- uses: foundry-rs/foundry-toolchain@v1
74+
with:
75+
version: stable
76+
77+
- uses: actions/setup-python@v5
78+
with:
79+
python-version: '3.12'
80+
81+
- name: Install Halmos
82+
run: pip install halmos
83+
84+
- name: Symbolic proofs
85+
run: halmos --match-contract HeadlessHalmosTest
86+
87+
# ────────────────────────── Tier 6 ────────────────────────────────
88+
# Mutation testing — slow (~15 min), runs only on:
89+
# • manual workflow_dispatch from the Actions tab, OR
90+
# • a pull request labelled `run-mutation`
91+
mutation:
92+
name: Tier 6 · Mutation testing (on label or dispatch)
93+
runs-on: ubuntu-latest
94+
if: |
95+
github.event_name == 'workflow_dispatch' ||
96+
contains(github.event.pull_request.labels.*.name, 'run-mutation')
97+
steps:
98+
- uses: actions/checkout@v4
99+
with:
100+
submodules: recursive
101+
102+
- uses: foundry-rs/foundry-toolchain@v1
103+
with:
104+
version: stable
105+
106+
- uses: actions/setup-python@v5
107+
with:
108+
python-version: '3.12'
109+
110+
- name: Install slither-mutate
111+
run: pip install slither-analyzer
112+
113+
- name: Generate mutants (8 operator categories, ~328 mutants)
114+
run: |
115+
slither-mutate src/Headless.sol \
116+
--test-cmd "forge test --no-match-contract 'Headless(Invariant|Halmos)' -q" \
117+
--output-dir mutation_campaign \
118+
--timeout 120 || true
119+
echo "Generated $(ls mutation_campaign/Headless/ 2>/dev/null | wc -l) mutants"
120+
121+
- name: Run custom mutation driver
122+
run: bash mutation_run.sh
123+
124+
- name: Upload mutation results
125+
if: always()
126+
uses: actions/upload-artifact@v4
127+
with:
128+
name: mutation-results
129+
path: mutation_results/

‎README.md‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,8 @@
11
# Headless (HDLS)
22

3+
[![verify](https://github.com/dreliq9/headless/actions/workflows/verify.yml/badge.svg)](https://github.com/dreliq9/headless/actions/workflows/verify.yml)
4+
[![License: AGPL v3](https://img.shields.io/badge/License-AGPL_v3-blue.svg)](https://www.gnu.org/licenses/agpl-3.0)
5+
36
> An autonomous, agent-native token. Written end-to-end by **Claude** (Anthropic's AI) at the prompt of a non-coder. No human wrote a line of the contract, the tests, or the verification stack.
47
58
**Status:** pre-audit, unaudited, not deployed. This is a verified code artifact, not a live protocol. **Do not put real ETH into this contract.** See [Safety](#safety) below.

0 commit comments

Comments
 (0)