Formal verification for policy module: 3 bugs fixed, 44 Z3 proofs, 100% MC/DC#7932

Open

buger wants to merge 28 commits intomasterfrom

experiment/formal-requirements-policy

Commits on Apr 20, 2026

experiment: formal requirements specification for internal/policy package

buger
and
claude
committed
Add Z3 boundary test fixtures and refactor test suite

buger
and
claude
committed
Remove generated docs from PR

buger
and
claude
committed
Polish test suite: remove redundancy, wire property fixtures, document FLIP

buger
and
claude
committed
Rename reqforge to reqproof across all spec files

buger
and
claude
committed
Remove unused fixtures, add requirement traceability annotations

buger
and
claude
committed
Remove meta-test TestZ3_FixturesExist

buger
and
claude
committed
Complete formal verification: obligations, Z3, MC/DC, verification_scope

buger
and
claude
committed
Push to L3 assurance: 99.5% coverage, 89.2%/91.3% MC/DC, all checks clean

buger
and
claude
committed
Remove generated artifacts from repo, add to .gitignore

buger
and
claude
committed
Achieve L3 assurance with strict MC/DC: 100% code MC/DC, MCDC witnesses, native Go test JSON

buger
and
claude
committed
L5 assurance: 100% MC/DC, 100% coverage, obligation checklists complete

buger
and
claude
committed
Add MCDC row witness annotations to all test files with Verifies links

buger
and
claude
committed
Enable test_mcdc_annotations check for strict MCDC enforcement

buger
and
claude
committed
Remove fixture_evidence.components — fixtures not committed to repo

buger
and
claude
committed
Adapt test helpers to PolicyID interface change from master

buger
and
claude
committed
Update trace link reviews after rebase on master

buger
and
claude
committed
Annotate and cover new MCP/policy code from main rebase

buger
and
claude
committed
Remove Z3 fixtures from repo — generated artifacts

buger
and
claude
committed

Commits on Apr 23, 2026

chore: fix spec lint warnings — AC cross-refs, tombstone, review metadata

buger
and
claude
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Formal verification for policy module: 3 bugs fixed, 44 Z3 proofs, 100% MC/DC#7932

Formal verification for policy module: 3 bugs fixed, 44 Z3 proofs, 100% MC/DC#7932
buger wants to merge 28 commits intomasterfrom
experiment/formal-requirements-policy

Commits on Apr 20, 2026

experiment: formal requirements specification for internal/policy package

Add Z3 boundary test fixtures and refactor test suite

Remove generated docs from PR

Polish test suite: remove redundancy, wire property fixtures, document FLIP

Rename reqforge to reqproof across all spec files

Remove unused fixtures, add requirement traceability annotations

Remove meta-test TestZ3_FixturesExist

Complete formal verification: obligations, Z3, MC/DC, verification_scope

Push to L3 assurance: 99.5% coverage, 89.2%/91.3% MC/DC, all checks clean

Remove generated artifacts from repo, add to .gitignore

Achieve L3 assurance with strict MC/DC: 100% code MC/DC, MCDC witnesses, native Go test JSON

L5 assurance: 100% MC/DC, 100% coverage, obligation checklists complete

Add MCDC row witness annotations to all test files with Verifies links

Enable test_mcdc_annotations check for strict MCDC enforcement

Remove fixture_evidence.components — fixtures not committed to repo

Adapt test helpers to PolicyID interface change from master

Update trace link reviews after rebase on master

Annotate and cover new MCP/policy code from main rebase

Remove Z3 fixtures from repo — generated artifacts

Commits on Apr 23, 2026

chore: fix spec lint warnings — AC cross-refs, tombstone, review metadata

Commits on Apr 24, 2026

Merge branch 'master' into experiment/formal-requirements-policy

fix: restore errcheck-compliant error handling with mcdc:ignore, reach 100% MC/DC

chore: update trace links and reviews after MC/DC coverage closure

feat: add property-based obligation classes with 12 new SYS-REQs

feat: fully cover 12 obligation SYS-REQs with tests and formalization

Commits on Apr 25, 2026

test: fix SYS-REQ-055 determinism test to actually catch QuotaRenews bug

fix: non-deterministic QuotaRenews due to map iteration order

chore: remove accidentally committed CI doc