Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0

### Added
- ADR-0007 (Accepted): claims-to-evidence discipline & optional-dependency policy — every headline claim maps to code+test or is labelled experimental; optional NIF deps are experimental-until-wired. Closes the recurring `doc-reality-drift` blocker. Earn-the-Core epic #53
- ADR-0008 (Proposed): formal-proof enforcement vs. scoping the "formally verified" claim — frames the maintainer decision (wire enforcement / scope the claim / hybrid), does not pre-decide it
- ADR-0008 (Accepted, Option C): scope the "formally verified" claim now (per ADR-0007) and fund a single-module runtime-enforcement PoC (issue #55)
- Earn-the-Core foundational-hardening program filed as tracked issues (#53 epic; #48–#52 children)
- ADR-0006: scoped and formally declined `proven-frame` hardening of `Burble.Bolt.Packet` (category mismatch — stream-framing core vs. a single-datagram record already total/safe via BEAM binary matching); closes the ADR-0005 backlog item
- Typed `NifEvent` ADT for Zig NIF audio events (VadStateChange, AgcLevelChange, DenoiserConfidence)
Expand Down
21 changes: 13 additions & 8 deletions docs/decisions/0008-formal-proof-enforcement-vs-scope.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,11 @@ Date: 2026-05-19

## Status

Proposed
Accepted — **Option C (hybrid)**, decided 2026-05-19 by the maintainer.

This ADR frames a genuine open strategic decision for the maintainer; it
deliberately does **not** pre-decide it. Part of the "Earn the Core"
program.
Part of the "Earn the Core" program. Follow-through tracked by issue
#55 (single-module enforcement PoC) and issue #51 (claim wording,
per ADR-0007).

## Context

Expand All @@ -33,7 +33,11 @@ closed or scoped honestly; which one is a strategic choice with real cost.

## Decision

**To be decided by the maintainer.** Options:
**Decided: Option C (hybrid).** Scope the claim immediately (Option B
wording, governed by ADR-0007 / issue #51) **and** fund a single-module
runtime-enforcement proof-of-concept before committing to the full
Idris2->runtime bridge (tracked by issue #55). The options
considered:

* **Option A — Wire enforcement.** Build the Idris2→runtime enforcement
bridge (proof-derived validators at the Elixir/Zig ABI boundary) as a
Expand Down Expand Up @@ -64,6 +68,7 @@ as a funded, scoped experiment rather than perpetual aspiration.

### Neutral

- Until accepted, ADR-0007 governs: the "formally verified" claim must
read as type-check-level only, with runtime enforcement labelled
Experimental/Aspirational.
- ADR-0007 governs the interim: the "formally verified" claim reads as
type-check-level only, runtime enforcement labelled
Experimental/Aspirational, until the PoC (issue #55) reports back
with a full-bridge go/no-go recommendation.
2 changes: 1 addition & 1 deletion docs/decisions/README.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -42,5 +42,5 @@ New ADRs copy `0000-template.adoc` and take the next number.

| link:0008-formal-proof-enforcement-vs-scope.adoc[0008]
| Formal-proof enforcement vs. scoping the "formally verified" claim
| Proposed
| Accepted (Option C)
|===
Loading