A formal verification is in progress, which is intended to cover at least soundness of the Action circuit used by the Orchard and Ironwood pools, before the NU6.3 upgrade that activates the latter. An important part of this effort will be to clearly and accurately document the scope of what is and is not formally verified.
The formalization is a Lean 4 development over Mathlib, and building it
re-elaborates every proof — a successful build is the verification. The single
command is lake build --wfail, with two one-time prerequisites: install
elan (the Lean toolchain manager, which
reads lean-toolchain and installs the pinned toolchain
automatically), then, from the repository root, fetch Mathlib's prebuilt
artifacts so it need not be recompiled from source:
lake exe cache get # one-time: download prebuilt Mathlib artifacts
lake build --wfail # verify every proof; --wfail makes warnings fail, as CI doesCI runs the same build plus source-level consistency checks — census coverage, fixture digests, and regeneration diffs — documented in Build and CI Checks.
Copyright 2026 Zcash Protocol Developers.
All code in this workspace is licensed under either of
- Apache License, Version 2.0, (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
- MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)
at your option.
Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.