Experiment with F* formally verified components generated via Claude#3236

Draft

Stringy wants to merge 18 commits intomasterfrom

giles/formal-verification

Commits on Apr 17, 2026

refactor: rename VerifiedNRadix to NRadixSpec as non-extractable spec

Stringy
and
claude
committed
feat: add find_returns_supernet and insert_then_find lemmas to NRadixSpec (admitted)

Stringy
and
claude
committed
feat: add NRadixPulse Pulse module with types and ghost invariant

Stringy
and
claude
committed
feat: add create and destroy operations to NRadixPulse

Stringy
and
claude
committed
feat: add is_empty to NRadixPulse

Stringy
and
claude
committed
feat: add find operation to NRadixPulse

Stringy
and
claude
committed
feat: add insert operation to NRadixPulse

Stringy
and
claude
committed
feat: extract NRadixPulse to C via Karamel

Stringy
and
claude
committed
feat: add verified static library CMake target

Stringy
and
claude
committed
feat: replace NRadix internals with verified Pulse implementation

Stringy
and
claude
committed
fix: remove parent-scope definitions from verified library build

Stringy
and
claude
committed
feat: add try_insert to NRadixPulse for duplicate detection

Stringy
and
claude
committed
feat: use try_insert for duplicate detection in NRadix wrapper

Stringy
and
claude
committed
fix: correct IsAnyIPNetSubset to use Find(IPNet) not Find(Address)

Stringy
and
claude
committed
chore: add .gitignore for F* build artifacts

Stringy
and
claude
committed
chore: add NetworkTypes and NetworkOps F* sources to version control

Stringy
and
claude
committed
chore: add add-verified-component skill

Stringy
and
claude
committed
docs: update add-verified-component skill for Pulse/ghost-spec approach

Stringy
and
claude
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Experiment with F* formally verified components generated via Claude#3236

Experiment with F* formally verified components generated via Claude#3236
Stringy wants to merge 18 commits intomasterfrom
giles/formal-verification

Commits on Apr 17, 2026

refactor: rename VerifiedNRadix to NRadixSpec as non-extractable spec

feat: add find_returns_supernet and insert_then_find lemmas to NRadixSpec (admitted)

feat: add NRadixPulse Pulse module with types and ghost invariant

feat: add create and destroy operations to NRadixPulse

feat: add is_empty to NRadixPulse

feat: add find operation to NRadixPulse

feat: add insert operation to NRadixPulse

feat: extract NRadixPulse to C via Karamel

feat: add verified static library CMake target

feat: replace NRadix internals with verified Pulse implementation

fix: remove parent-scope definitions from verified library build

feat: add try_insert to NRadixPulse for duplicate detection

feat: use try_insert for duplicate detection in NRadix wrapper

fix: correct IsAnyIPNetSubset to use Find(IPNet) not Find(Address)

chore: add .gitignore for F* build artifacts

chore: add NetworkTypes and NetworkOps F* sources to version control

chore: add add-verified-component skill

docs: update add-verified-component skill for Pulse/ghost-spec approach