Repository navigation
Conversation
Replace the trust engine's pure core with a Dafny-verified kernel,
extracted to Rust and dropped in behind the `verified-kernel` cargo
feature. With the feature off (default) the native fixed-point engine is
unchanged; with it on, Derivation::derive routes through the kernel and
the existing unit and e2e tests run against it.
The kernel is built with Veri, an experimental verification system: the
spec is written in the Veri DSL and compiled through its Dafny -> Rust
toolchain.
- src/trust_engine.veri.md: the Veri DSL spec of the derivation core
(believed names + constraint delegation, IPs, authz, pattern-resolved
endorser/target), carrying the types and contracts.
- src/trust_engine/kernel/: the verified TrustEngine.dfy and its
Dafny -> Rust extraction, as a self-contained crate excluded from the
workspace (its own vendored dafny_runtime).
- src/trust_engine/{marshal,runner}.rs: intern intermesh types into the
kernel's relations, run it, and marshal results back into Derivation,
keeping derive's signature identical.
- finalize/expand_authz_side/imids_in_pattern move out of the native-only
impl so both paths share them; MAX_DERIVATION_ITERATIONS is localized
to the native loop.
- .veri/veri.toml maps the spec to its committed output dir; xtask
forwards INTERMESH_FEATURES so the e2e binary can build the kernel.
KerneyJ
force-pushed
the
verify-trust-engine
branch
from
June 30, 2026 19:31
db084bb to
d90142b
Compare
KerneyJ
marked this pull request as ready for review
June 30, 2026 22:44
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Replaces the trust engine's pure core with a formally verified kernel, behind the verified-kernel cargo feature. Feature off (default): the native engine is unchanged. Feature on: derive routes through the kernel and the existing unit + e2e tests run against it.
The kernel is written as a spec in the Veri DSL (src/trust_engine.veri.md), compiled to Dafny. The correctness invariants (monotonicity, commutativity, and termination) are proven at build time. Dafny then transpiles the proven program to Rust. Most of the added lines are the Dafny runtime the transpiled Rust links against. The hand-written code to review is the spec, plus the marshalling (marshal.rs) and runner (runner.rs) that wire the kernel into derive.