Support verifying a library main contract via a generated harness - #132

Merged

shellygr merged 15 commits into

shelly/library-harness

Sep 11, 2026

Commits on Aug 7, 2026

Add the library harnesser: make a library main contract verifiable

shellygr
and
claude
committed
d033023
Verify a generated harness when the main contract is a library

shellygr
and
claude
committed
b010ba2
Drop the wrapped library's own qualifier from generated identifiers

shellygr
and
claude
committed
87b1c05

Commits on Sep 5, 2026

Give storage readers their data location

shellygr
and
claude
committed
a0800c9
Resolve the probe build's packages instead of letting certora-cli guess

shellygr
and
claude
committed
6cb3250
Keep the wrapped library in the conf's scene

shellygr
and
claude
committed
f2c8199
Merge master into the library harnesser

shellygr
and
claude
committed
410adae
Never summarize the library a harness wraps

shellygr
and
claude
committed
2833523
Do not let a conf list the same contract twice

shellygr
and
claude
committed
96e7490

Commits on Sep 6, 2026

Share one CVL keyword list between the harnesser and summaries

shellygr
and
claude
committed
c036c78
Share what the harnesser had written for itself

shellygr
and
claude
committed
71389a8

Commits on Sep 10, 2026

Merge remote-tracking branch 'origin/master' into shelly/library-harness
shellygr
committed
b73886a
Address the second review pass

shellygr
and
claude
committed
4c3b255

Commits on Sep 11, 2026

Merge branch 'master' into shelly/library-harness
shellygr
authored
0657323
Merge branch 'master' into shelly/library-harness
shellygr
authored
7db7d4a