Verify doc-owned specifications over recursive mathematical models

.gitattributes

@@ -0,0 +1,4 @@
+# Preserve complete generated Lean snapshots, including literal bytes. Aeneas's
+# pretty printer can emit trailing code spaces; the conservative comparison and
+# independent proof builds check these files instead of hand-formatting them.
+verification/aeneas/golden/*.lean whitespace=-blank-at-eol

.github/workflows/ci.yml

@@ -1052,6 +1052,71 @@ jobs:
           name: ${{ env.ZC_CI_IMAGE_ARCHIVE }}
           path: ${{ runner.temp }}/${{ env.ZC_CI_IMAGE_ARCHIVE }}
 
+  aeneas:
+    name: Aeneas translation and Lean proofs
+    runs-on: ubuntu-24.04
+    timeout-minutes: 90
+    env:
+      # Charon uses its own pinned Rust compiler. Keep the ordinary Rust CI
+      # flags (including randomized layouts) out of this extraction.
+      RUSTFLAGS: ""
+      RUSTDOCFLAGS: ""
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
+
+      - name: Install rustup
+        uses: dtolnay/rust-toolchain@02cb101ec7c40f2c49e1d9714d64511d8e1b74de # zizmor: ignore[superfluous-actions]
+        with:
+          toolchain: stable
+
+      - name: Install Nix for the pinned Aeneas source build
+        uses: DeterminateSystems/determinate-nix-action@8d87e8d5e5b8a8309d4281094560f127d9a265f1 # v3.22.5
+
+      - name: Install the pinned Aeneas, Charon, Rust, and Lean bundle
+        run: bash verification/aeneas/setup.sh
+
+      - name: Test Rust syntax ownership, discovery, and golden comparison
+        run: |
+          source verification/aeneas/toolchain.sh
+          export CARGO_TARGET_DIR="$PWD/target/aeneas/annotation-tool"
+          cargo +"$AENEAS_RUST_TOOLCHAIN" test --locked --manifest-path tools/Cargo.toml -p aeneas-inline
+          cargo +"$AENEAS_RUST_TOOLCHAIN" build --locked --manifest-path tools/Cargo.toml -p aeneas-inline
+          python3 -B -m unittest discover -s verification/aeneas/tests
+
+      - name: Check nominal type extraction and upstream compatibility
+        run: bash verification/aeneas/tests/nominal-tuples.sh
+
+      # run.sh checks the same contracts against two definition sets. Keep
+      # negative controls after this positive baseline: a missing dependency
+      # or an already broken proof cannot count as rejection of a mutation.
+      - name: Compare live extraction with goldens and prove both models
+        run: bash verification/aeneas/run.sh
+
+      - name: Test compiled effective-spec inspection
+        run: |
+          source verification/aeneas/toolchain.sh
+          export PATH="${AENEAS_TOOLCHAIN_DIR:-$PWD/target/aeneas/toolchain}/lean/bin:$PATH"
+          export AENEAS_INSPECTION_PROJECT="$PWD/target/aeneas/verification"
+          python3 -B -m unittest discover -s verification/aeneas/tests -p test_inspect.py
+
+      - name: Verify that admissions and incorrect code fail
+        env:
+          LEAN_NUM_THREADS: "2"
+        run: |
+          # Each suite mutates only its own generated project. Collect both
+          # statuses so a failure cannot leave the other suite unobserved.
+          bash verification/aeneas/negative-controls.sh golden-verification > target/aeneas/golden-controls.log 2>&1 &
+          golden_pid=$!
+          bash verification/aeneas/negative-controls.sh verification > target/aeneas/live-controls.log 2>&1 &
+          live_pid=$!
+          status=0
+          wait "$golden_pid" || status=1
+          wait "$live_pid" || status=1
+          cat target/aeneas/golden-controls.log target/aeneas/live-controls.log
+          exit "$status"
+
   # Used to signal to branch protections that all other jobs have succeeded.
   all-jobs-succeed:
       # WARNING: This name is load-bearing! It's how GitHub's settings UI configures which jobs
@@ -1062,7 +1127,7 @@ jobs:
       # success in branch protection, so this aggregation must fail closed.
       if: ${{ always() }}
       runs-on: ubuntu-latest
-      needs: [build_test, miri, codegen, coverage, kani, check_be_aarch64, check_avr_atmega, check_fmt, check_actions, check_readme, check_versions, check_msrv_is_minimal, check_stale_stderr, check-all-toolchains-tested, check-job-dependencies, check-todo, run-git-hooks, zizmor, build_docker_env]
+      needs: [aeneas, build_test, miri, codegen, coverage, kani, check_be_aarch64, check_avr_atmega, check_fmt, check_actions, check_readme, check_versions, check_msrv_is_minimal, check_stale_stderr, check-all-toolchains-tested, check-job-dependencies, check-todo, run-git-hooks, zizmor, build_docker_env]
       steps:
         - name: Reject workflow cancellation
           if: ${{ cancelled() }}

.gitignore

@@ -10,6 +10,28 @@
 target
 lcov.info
 
+# Generated inputs and caches for the native Aeneas proof development project.
+verification/aeneas/__pycache__/
+verification/aeneas/lean/.lake/
+verification/aeneas/lean/lakefile.lean
+verification/aeneas/lean/lake-manifest.json
+verification/aeneas/lean/lean-toolchain
+verification/aeneas/lean/Specs.lean
+verification/aeneas/lean/ModelShapes.lean
+verification/aeneas/lean/Models.lean
+verification/aeneas/lean/Required.lean
+verification/aeneas/lean/Specs.source-map.json
+verification/aeneas/lean/ModelShapes.source-map.json
+verification/aeneas/lean/Models.source-map.json
+verification/aeneas/lean/Specs.sources.sha256
+verification/aeneas/lean/.inline-projections.json
+verification/aeneas/lean/bindings.json
+verification/aeneas/lean/proof-dependencies.json
+verification/aeneas/lean/Zerocopy/Types.lean
+verification/aeneas/lean/Zerocopy/Funs.lean
+verification/aeneas/lean/Zerocopy/TypesExternal_Template.lean
+verification/aeneas/lean/Zerocopy/FunsExternal_Template.lean
+
 # VSCode workspace files
 *.code-workspace
 

skills/zerocopy-review/SKILL.md

@@ -54,6 +54,44 @@ Check the issues that are relevant to the changed behavior, including:
 Before suggesting a new dependency, check `Cargo.toml` and the existing
 workspace for an appropriate dependency or utility.
 
+## Specification Meaning
+
+For every specification under review, reconstruct the guarantee a human likely
+intends. Ground that interpretation in the specification, surrounding
+documentation, callers, reference implementations, and the bug or change that
+motivated it. Compare the intended guarantee with what the specification
+actually states. A passing proof establishes the written proposition; it does
+not establish that the proposition captures the intended behavior.
+
+Look for ways the written guarantee could be weaker than that intention:
+
+- Requirements, ghost parameters, or branch guards exclude intended inputs.
+  Inconsistent requirements, a ghost parameter with an empty type, or an
+  admission predicate that always returns `false` can make a claim vacuous:
+  there are no cases in which the promised behavior must hold.
+- Automatic input decoding or type-model invariants restrict the domain beyond
+  what a reader would reasonably infer from the function's specification.
+- Postconditions omit intended observations, or compare projections that
+  discard the information whose correctness matters.
+- An equivalence harness checks only successful results or skips comparisons
+  on relevant paths, leaving intended failure behavior or other cases unchecked.
+- A reference implementation shares the very logic whose correctness the
+  equivalence check is meant to establish.
+- A partial-correctness contract allows divergence where termination is
+  intended, or a proof covers fewer inputs or configurations than claimed.
+
+A total `ensures _ => True` can be sufficient for an assertion harness:
+successful termination requires its assertions to pass on admitted inputs.
+Inspect the assertions and admission conditions rather than rejecting the
+postcondition merely because it is `True`. Concrete admission examples can
+expose vacuity, but do not establish coverage of every intended input.
+
+Report substantiated gaps even when the proofs pass. State the intended
+guarantee, the weaker written claim, and a distinguishing case when possible.
+Keep inferred intention separate from the existing contract. When intention is
+unclear, make that uncertainty explicit and seek clarification when needed;
+do not silently invent a stronger requirement.
+
 ## Findings
 
 Report actionable findings, not private chain-of-thought. For each finding:

tools/Cargo.toml

@@ -8,6 +8,7 @@
 
 [workspace]
 members = [
+    "aeneas-inline",
     "cargo-zerocopy",
     "generate-readme",
     "ui-runner",

tools/aeneas-inline/Cargo.toml

@@ -0,0 +1,20 @@
+# Copyright 2026 The Fuchsia Authors
+#
+# Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+# <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+# license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+# This file may not be copied, modified, or distributed except according to
+# those terms.
+
+[package]
+name = "aeneas-inline"
+edition.workspace = true
+version.workspace = true
+license.workspace = true
+publish.workspace = true
+
+[dependencies]
+proc-macro2 = { version = "1", features = ["span-locations"] }
+rustc_lexer = "=0.1.0"
+serde_json = "1"
+syn = { version = "2", features = ["full", "visit"] }