Skip to content

Flagship Lean Witness v0.1.4 — End-to-End Formal Proof + Deterministic Container Repro

Choose a tag to compare

View all tags
@inaciovasquez2020 inaciovasquez2020 released this 09 Feb 14:28
· 277 commits to main since this release
v0.1.4
c94c8bf

Flagship Lean Witness v0.1.4

This release freezes the first end-to-end formally verified Lean witness chain together with a deterministic container reproducibility environment and external CI verification.

Verification surface (complete tuple)
• Lean formal proof: green build, zero sorry
• Toolchain pin: lean-toolchain
• Dependency resolution: lake-manifest.json
• Container reproducibility: Dockerfile + IMAGE_DIGEST
• Integrity: MANIFEST.sha256
• External witnesses:
– Lean CI rebuild
– Container rebuild CI
– Nightly adversarial dependency stress CI

Container mirrors
• GHCR: ghcr.io/inaciovasquez2020/flagship-lean:repro-v0.1.4
• Docker Hub: inaciovasquez2020/flagship-lean:repro-v0.1.4

Reproduction (local)
lake update
lake build

Reproduction (container)
docker pull ghcr.io/inaciovasquez2020/flagship-lean:repro-v0.1.4
docker run --rm ghcr.io/inaciovasquez2020/flagship-lean:repro-v0.1.4

Security / determinism guarantees
• Toolchain pinned
• Dependency graph snapshot published
• Manifest integrity published
• Independent CI rebuild required for acceptance

Counterexample defense layer
• Enumeration harness scaffold
• Property-based generator scaffold
• Nightly dependency drift stress build

Intended use
• Formal verification reference artifact
• Referee reproducibility package
• Independent third-party replication base

Author
Inacio F. Vasquez
Independent Researcher (Foundations of Physics & Mathematics)

Assets 7
Loading