The Verification Foundry · a working demonstration
Make AI-assisted verification
easier to review.
Freeze the claim. Inspect the assumptions. Run the named checks. Hand another engineer the inputs, results and limits they need to evaluate the work.
Working browser demonstrations and recorded formal evidence, with the status of each method made explicit.
▸ Start with one bounded task from your existing verification workflow. Evaluate whether a clearer evidence handoff reduces review effort at the same acceptance bar.
the signal path
A human defines the claim and assumptions. Each result records its method and scope. Reviewers decide whether that evidence supports the intended use.
Live · TypeScript graph-policy demonstration
The capDL isolation lab
Explore a small graph model of capability connections. The TypeScript checker compares each edge with the selected policy and reports forbidden edges. This is a teaching model, not an upstream capDL validator or a proof of a deployed seL4 system.
Provenance: this is a system-composition example we ported to make the checker legible, not an seL4 or capDL deliverable. The engine below is real and runs here; the framing is a proposed port. Section 09 says so again, unprompted.
Four protection domains. Driver contains tcb and frame; App contains tcb and frame; Channel contains endpoint; Secret is isolated and contains secret. Current capability edges: driver.tcb to driver.frame; driver.tcb to channel.endpoint; app.tcb to channel.endpoint; app.tcb to app.frame. Secret is not reachable from app.tcb.
inject
readout
- verdict
- true
- violating edge
- —
- secret reachable from app
- no
- base edges
- 4 permitted
policy · mayConnect
same-domain edges are always permitted (the relation is reflexive).
Related model theorem: CapDLIsolation.checkIsolation_correct — recorded Lean evidence. This browser runs TypeScript; correspondence to that theorem is not established.
export
The certificate carries the graph, the policy it was checked against, the verdict and the reachability result — everything a third party needs.
current: ACCEPTED · policy permits driver<->channel, app<->channel
re-check a certificate
nothing re-checked yet.
Recomputed graph checks under the certificate’s declared policy. This does not approve that policy or authenticate the sender.
Live Z3 checks · recorded Lean comparison
Run the checks. Inspect each method.
This demonstration compares three live Z3 results with recorded Lean results. Z3 runs here as WebAssembly and really discharges these three obligations; the second column is an attested, recorded verdict from AXLE — our Lean 4 corpus of machine-checked algebra and access-control lemmas, carried over from prior mathematics work and re-checkable in Lean, not here. Honest scope: these three are small and decidable; the harder theorems rest on one re-checker, and we say so.
The live checks have not been run.
xor_otp_involution
theory: bitvector
(m ⊕ k) ⊕ k = m
Z3 assertion: m, k : BitVec 8 ⊢ assert (m ^ k) ^ k ≠ m
- Z3 · live
- idle
- Lean/AXLE · attested
- proved (recorded)
agreement · pendingdefault_deny
theory: boolean
no grants ⇒ no access
Z3 assertion: inScope, isPriv, isUnowned : Bool ⊢ assert ¬inScope ∧ ¬isPriv ∧ ¬isUnowned ∧ (inScope ∨ isPriv ∨ isUnowned)
- Z3 · live
- idle
- Lean/AXLE · attested
- proved (recorded)
agreement · pendingunauth_write_frame
theory: array
unauthorized write → no change
Z3 assertion: mem : Array(Int,Int); a, v, x : Int; auth : Bool ⊢ assert ¬auth ∧ If(auth ∧ x=a, v, mem[x]) ≠ mem[x]
- Z3 · live
- idle
- Lean/AXLE · attested
- proved (recorded)
agreement · pending
Z3 is really solving these in your browser — inspect the encodings; they are the negations of the claims, and unsat is the solver verdict. No proof object is independently checked here. The Lean/AXLE row is a recorded result from our verified corpus, not a live run: two live independent provers is Phase 1.
Interactive teaching model · selected labels
The honesty taxonomy
Explore the labels used to describe evidence. Selecting a label does not earn it. This browser exercise illustrates a review policy; it does not run a compiler or independently establish the selected assurance level.
selected grade
AGRADE(AI-proposed-and-unchecked)
A draft artifact. An unchecked expansion of the trusted base.
promotion attempt
The button displays an example review rule. No compiler runs here.
Live · signed in your browser
The certificate receipt
The certificate is the product, so here it is for the state currently on this page: a canonical JSON record of every input and verdict above, signed with HMAC-SHA-256 by Web Crypto in your browser. The key is a published demonstration key, so the receipt retains the legacy attested label for compatibility. Anyone can alter and re-sign it. This demonstrates byte consistency, not authenticated origin or proof that a check was executed.
actions
No receipt issued yet.
signature
- algorithm
- HMAC-SHA-256 over sorted-key JSON
- key id
- verification-foundry/demo-hmac-key/v1
- digest
- —
signer identity · optional
The HMAC key is published, so it cannot establish identity. Generate a P-256 key in this tab to add an ECDSA signature over the payload, then export the public half for the verifier to obtain independently.
- key thumbprint
- —
- identity signature
- not attached
shareable state
?grade=4
// press “issue signed receipt” to sign the current inputs and verdicts
import & verify
Drop, paste or upload a downloaded certificate
The importer first validates the document against a strict schema and reports the exact line and column of anything missing or mistyped. It then recomputes the SHA-256 over the canonical JSON (excluding its own content_hash), re-derives the HMAC-SHA-256 over the embedded payload, optionally verifies an asymmetric signer identity against a public key you supply, and — on RE-CHECK — re-runs the real client-side checkers against the inputs the certificate records.
drag a .json certificate anywhere onto this box, or paste it — the box is focused on load
Leave this empty and identity stays UNVERIFIED by construction: the HMAC key is published, and a public key shipped inside the certificate it verifies is self-attested.
Nothing imported yet.
// paste a receipt or an isolation certificate, then press verify. Failures are reported line by line; nothing is trusted because it looks official.
verification history · local to this browser
no runs recorded yet — every verify and re-check is appended here
Live · authority propagation
Watch authority spread — and prove where it can't.
The take-grant model is the classic account of how capability authority propagates. Step the rewrite rules and watch de-facto authority grow; then ask the confinement question — can subject A ever acquire a right over B? Disconnected islands are provably safe. This is our TakeGrant.authority_confined theorem, made operable.
Subjects s1, s2, s3 and objects o1, o2. Current edges: s1 read o1; s2 take s3; s3 read o2.
rewrite rules
- take: x -t-> y ∧ y -α-> z ⟹ x -α-> z
- grant: x -g-> y ∧ x -α-> z ⟹ y -α-> z
confinement query
no query run yet.
The reachable authority is contained in the take-grant closure (a sound over-approximation). Two subjects in disconnected islands can never share authority. The closure and every confinement answer above are computed here, in your browser — not a mock-up.
Interactive teaching model · declared component labels
Inspect the assumptions between components.
This exercise takes the lowest of the labels you assign and flags declared assumptions. It is a planning heuristic, not a proof of system assurance. Actual composition requires compatible semantics and evidence that each component's guarantees satisfy the next component's assumptions.
| component | grade | in TCB | AI spec | |
|---|---|---|---|---|
| proof · rank 4 | ||||
| partial · rank 2 | ||||
| attested · rank 3 | ||||
| attested · rank 3 |
illustrative minimum label
minimum over 4 component(s) · rank 2
trusted computing base
- SMT backend (Z3)
- Cryptol spec of HMAC
- compiler
warnings
- · Illustrative minimum label is set by: SMT backend (Z3).
Marking a trusted component’s specification as AI-authored changes the illustrative label and warnings. These calculations run in the browser; they do not establish whole-system assurance.
Load-bearing claims
What a useful handoff contains
These are the proposed working practices to evaluate on one concrete task. The demonstrations below do not establish production readiness.
An explicit claim
Record the intended behavior, source revision and assumptions before evaluating a candidate. A changed specification needs a new review.
Method by method evidence
Distinguish a solver verdict, a recorded proof result, a fresh kernel check and a human decision. Each answers a different question.
A reproducible handoff
Keep inputs, commands and limitations with the result. A digest binds bytes; a public demonstration signing key cannot authenticate the sender.
A measurable pilot
Evaluate one bounded task in the team's existing tools. Measure review time, failed checks and unresolved assumptions before expanding the scope.
Fit · build-with, not build-versus
Where this sits in your stack
A focused engineering engagement around one task in your existing workflow. Your team defines the claim and acceptance criteria; we build and evaluate the evidence handoff together.
Where this attaches
Aerospace, defense, and critical systems
The first landing is any work already under a formal obligation: safety software, kernels, separation architectures, or cryptographic cores. The useful program artifact is evidence a third party can re-check using documented inputs, commands and the required tool environment.
What open tooling already provides
Specifications, provers, and checkers
Open high-assurance workflows already provide formal specifications, symbolic execution, theorem proving, and machine-readable proof artifacts. None of that needs to be replaced; this layer makes agreement and provenance travel with the result.
What we add
The gate, the grade, the certificate
A prototype evidence handoff: explicit claims, named assumptions, method attribution and reproducible checks. Production adapters and independently enforced acceptance policy remain work to evaluate with a technical owner.
Explicit claims, attributed results, stated assumptions and reproducible commands support independent review.
Honest limits · stated unprompted
We raise the objections first
A high-assurance audience trusts the caveats more than the claims. These are stated up front, unprompted — the discipline is the pitch.
Agreement is not independence
Provers can share an SMT-LIB frontend or bit-blasting core, so bugs can correlate. The honest claim is “not the same bug,” never a soundness proof.
The spec stays trusted
Cross-prover agreement does nothing about a wrong hand-written Cryptol spec. Putting AI on the toil changes labor cost, not the trust boundary.
The kernel and implementation stay trusted
A certificate records exactly what was checked and what remains assumed. It does not turn a bounded model or a browser demo into a proof of an entire implementation or kernel.
Demo-or-die
The proof-of-life is a real obligation cleared by independent checkers with a re-checkable certificate. Until a reproducible artifact backs a larger claim, it remains a bounded demonstration.
No numbers yet
No throughput, coverage, or integration claim until a reproducible artifact backs it.
A second checker is not magic
Independent cores can share frontends or assumptions, so agreement is not a soundness proof. The honest claim is a visible, machine-checked precondition and a portable record of the remaining trust boundary.
Existing tools remain the authority
The gate is intentionally additive: it does not replace formal methods, proof review, or the checker that owns the underlying theorem.
The open program
Three phases, in order
Sequenced so that the cheapest falsification comes first: if phase one fails, the rest is correctly abandoned.
Phase 1 · proof-of-life
01One bounded obligation through the gate
Choose a small, already-understood formal obligation, run the identical statement through independent checkers, and issue a signed, re-checkable certificate. Success is narrow and falsifiable: a third party can re-check the record without the full pipeline.
Open-source research
02Deep provers meet a portable agreement gate
Keep the underlying specifications and proof systems authoritative; add a thin, open layer for agreement, provenance grading, and evidence that travels with the result.
Program attachment
03Evidence a program office can re-check
When the artifact is ready, attach the trust layer to a high-assurance workflow where reviewers need a compact, reproducible record rather than another dashboard.