docs_only · entailed
The assumption supports this check.
has_plan("payments") follows because it was explicitly assumed. The result is conditional on the declared theory, not independent confirmation that a plan exists.
Weft · executed development example
State the assumptions.
See what follows.
In the Writfold harness, Weft is the planning check. It assesses a declared theory, keeping what follows from your assumptions separate from what remains unknown — and from permission to change anything.
Runs today Local assessment · reports carry no write permission
01 / A small, explicit theory
A plan is not a successful restore.
This example assumes that the payments service has a plan. It asks whether that same fact follows, and whether a successful restore follows too. No rule connects the two.
Download review.weft · exact source used for this assessment
review recovery_plan {
context "unresolved-context" at "unresolved-release";
profile "weft.symbolic/1";
target change = proposal "unresolved-plan";
assume documented: has_plan("payments");
check docs_only: has_plan("payments");
check restore_works: restores("payments");
}
An assumption is an input, not evidence.
assume documented puts has_plan("payments") into the theory. The label does not mean Weft read a runbook or verified a service. Each check asks what follows from that declared theory.
02 / Actual assessment
Reading the result
This command was run with the development binary on the downloaded file. The binary is not published yet.
weft prove review.weft --json
restore_works · undetermined
The theory does not settle this check.
Neither restores("payments") nor its negation follows. Undetermined is not refuted: the example establishes neither a successful restore nor a failed one.
The report records each check with basis=hypothetical, the run as execution=complete, effect_authority=false, and that no Writfold evidence backs it.
weft prove exits 1 for every hypothetical result, even when all checks are entailed: the local tool has no success exit for a hypothetical report. Read the per-check outcomes, not the exit code.
03 / The assessment boundary
What Weft does and does not do
| Statement | Role | Result |
|---|---|---|
has_plan("payments") | assumed | given |
docs_only | check | entailed |
restore_works | check | undetermined |
A bounded logical claim.
Weft evaluates the declared finite theory. It does not prove an arbitrary implementation correct, extract all facts from prose, or demonstrate that a production restore works.
Evidence and authority remain separate.
A source-bound report is not evidence Writfold has established. Resolving real contexts and authorizing changes belong to Writfold. In Writfold's trial profile, a report can cite retained evidence by digest, is bound to a prepared edit, and can be required at approval (approve --require CHECK refuses unless that check is entailed); Writfold still records its results as hypothetical. Context resolution is not built yet.
Next: preparing a change.
Weft only assesses; it never edits. When a change is needed, Splicery prepares it as a byte-exact edit, and Writfold applies it only after approval.
Availability
Source only
Weft is built from source; there is no release binary. This page shows a local assessment, not Writfold integration. See the status page for what runs today.
Proved over the shipped Rust: Weft's set algebra (union, intersection, difference, membership, subset, normalisation), its verdict classification (entailed, refuted, undetermined, inconsistent) and its reuse comparison, which refuses any difference. Typing, provenance, budgets, quantifiers, lowering and reports are modelled and tested, not proved. How we know
Executed Weft binary SHA-256: 939e35badb2eea01b3723810b96563987332dde581ffd8960b0d353939537845. This identifies the development binary used; it is not a release download.