A Rust CLI Release Pipeline That Proves "Secrets Don't Leak" in Lean and Turns It Into a CI Gate

Why “Tests Are Green” Wasn’t Enough

I’m building a CLI tool that runs agents without ever handing them a real API key. The property I want to protect is simple: the child process must never receive the real key. If that breaks, there’s no point in using the tool at all.

But passing tests alone didn’t feel like enough assurance. All a test can say is “this input is fine,” not “any input is fine.” When you’re handling keys, that gap isn’t something you can ignore.

So I wrote proofs in Lean and had CI build them. It takes effort, but given what’s at stake I think it’s a reasonable investment. In this article I’ll walk through an excerpt of the CI/CD I set up. I’ve hidden the project-specific internal names and kept only the design and the mechanics.

The Numbers

One quiet but effective detail is that both sorry (a shortcut that leaves a proof unfinished) and axiom (an unproven assumption) are 0. It means the core invariant is proven all the way through rather than papered over with assumptions, and this is part of what CI requires to go green.

The CI Is Split Into Three Layers

┌─────────────────────────────────────────────┐
│ 1. Formal verification (core)               │
│    Prove "the child never gets the real key"│
│    in Lean — 28 theorems / sorry·axiom 0    │
├─────────────────────────────────────────────┤
│ 2. Safety-invariant gates × 11              │
│    deny-before-inject / DNS guard /         │
│    audit boundary / secret-type … —         │
│    one condition = one gate, machine-checked│
├─────────────────────────────────────────────┤
│ 3. General quality + supply chain           │
│    fmt / clippy -D warnings / test /        │
│    cargo-deny (advisories, bans, sources)   │
└─────────────────────────────────────────────┘

1. Prove the Core in Lean, and Build It in CI

The core property — “the child process never receives the real key” — lives as a proof under formal/lean. It’s 28 theorems and lemmas, with no sorry and no axiom among them. CI builds this proof every time and confirms that it passes with no shortcuts and no unproven assumptions.

For example, the core theorem takes this form. It states at the type level that “the result of sanitizing a real secret can never be a value that reaches the child process.”

theorem real_secret_is_not_sanitized_to_child
    {secret : Secret} {child : ChildValue} :
    sanitizeValue (InternalValue.realSecret secret) ≠ some child := by
  intro impossible
  cases impossible

The denial side is proven the same way (denied_request_never_calls_injector — a denied request never calls the injector). Where a test can only say “this input is fine,” theorems like these say “every input is fine.” I let CI carry that one extra step for me.

2. Make Everything Else “One Condition = One Gate”

The operational conditions I can’t take all the way to a proof are each turned into an independent check script and lined up as CI steps. There are 11 in all. I don’t bundle them into one giant test, because when something breaks I want to read which condition failed straight from the step name.

If a change breaks any of these conditions, the corresponding gate turns red on the spot.

Leak Smoke Test: Confirming Secrets Don’t Show Up in the Output

For a security tool, the accident I personally fear most is a secret accidentally leaking from a log or a diagnostic output. So I put a dummy secret into an environment variable, run the diagnostic command, and have CI confirm that the dummy value doesn’t appear in the output. What it does is crude, but that also makes it unambiguous (only the variable and tool names are generalized; the logic is close to the real thing).

- name: doctor json smoke
  env:
    SECRET_KEY: ci-dummy-secret
  run: |
    output="$(mktemp)"
    cargo run --quiet --bin <tool> -- doctor --json > "$output"
    # 1) fail immediately if the dummy secret appears in the output
    if grep -q "ci-dummy-secret" "$output"; then
      echo "secret leaked into doctor output" >&2
      exit 1
    fi
    # 2) the diagnostic's fail count must be 0
    test "$(jq '.summary.fail' "$output")" -eq 0

It’s just a “put a secret in, watch that it doesn’t come out” test, but it reliably closes off one way a leak could actually happen.

Supply Chain and Multiple OSes

Dependencies are left to cargo-deny, which looks at vulnerability advisories, banned crates, and the provenance of sources all together. Builds run mainly on Linux; the Windows and macOS smoke tests don’t run routinely and are started manually with workflow_dispatch only when needed. It’s a deliberate call that running the full matrix every time isn’t worth it.

Release: Build 5 Targets in a Matrix and Attach Checksums

The release runs on a tag push (v*). It builds 5 targets in a matrix: Linux (x86_64 / aarch64), macOS (x86_64 / aarch64), and Windows (x86_64). Only Linux aarch64 is cross-compiled with cross; macOS arm64 is a normal build.

After the build, the Unix binaries are stripped, and a smoke test confirms that the resulting archives (tar.gz / zip) actually contain the binary and the license. Finally, all targets are collected and a SHA256SUMS file is created with sha256sum and attached. Because the contents of the artifacts are inspected mechanically before they go out, it’s unlikely I’ll later discover that a license was left out or that one platform is missing.

Publishing: Nothing Ships Without Passing the Confirmation Phrase

Development happens in a private repository, and it is reflected to the public repository only when I manually invoke a dedicated publish workflow. To avoid shipping something by mistake, I’ve constrained the procedure like this:

1. Require a confirmation phrase to be entered at run time (if it doesn’t match, it stops there)
2. Copy only the files on the publish allowlist into the staging tree
3. Strip internal comments within staging (documentation comments are kept)
4. Run Trivy and the tests against staging
5. Reflect only a staging tree that has passed to the public repository

The pipeline enforces “develop in private, and publish only the parts that passed inspection.” With this in place, the accident of unreleased code or internal notes slipping into the public side is prevented by construction.

Wrapping Up

In the end, I think of a security tool’s CI/CD less as a place to check that things “work” and more as a place to confirm every time that nothing is broken. I divided the work so that the core invariant is left to Lean, and the remaining operational conditions are each checked by a gate.

If You Want to Copy This, Start Here

The Lean proofs are, honestly, a high bar to copy as-is. But the parts that pull their weight can be adopted far more cheaply.

• One condition = one gate: just turn each condition you want to protect into its own independent check script. When it fails, you know exactly what broke.
• Leak smoke test: a few-line test that puts in a dummy secret and uses grep to watch that it doesn’t come out. You can add it today, even without Lean.

Beyond “tests are green,” you stack up “if this condition breaks, turn CI red,” one at a time. Even that alone changes how much confidence the pipeline gives you.

If you have a project that needs this kind of work — designing CI/CD with formal verification built in, supply-chain hardening, or setting up Rust release workflows — feel free to reach out via Services.