mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zeekay
c86eec94cb
Local zoo/formal was a stale parallel checkout that pointed at
zoo-labs/formal (non-existent); the canonical remote is
zooai/proofs. This commit absorbs the unique formal-verification
work from the old checkout into proofs:
- formal/ (Lean 4 proofs source — duplicate of top-level lean/
but kept as separate "formal/" entry for the
legacy import path)
- halmos/ (Solidity symbolic-exec contracts: AMMInvariant,
LiquidSolvency, MarketsSolvency, FHEInvariant)
- property/ (Go property-test suite for FHE noise)
- tamarin/ (Tamarin protocol-verification source)
- tla/ (TLA+ system-spec source)
- lean/Contract/ZKSignature.lean (unique, not in proofs/lean)
- lean/Crypto/ZKSignature.lean (unique, not in proofs/lean)
- FORMAL_VERIFICATION.md (preserved from the old README)
- LLM-formal.md (preserved from the old LLM.md)
The duplicate folder /Users/z/work/zoo/formal is now deleted on
disk. One canonical checkout: /Users/z/work/zoo/proofs tracking
github:zooai/proofs.
64 lines
2.2 KiB
INI
64 lines
2.2 KiB
INI
\* Wave.cfg -- TLC / Apalache model checking configuration
|
|
\*
|
|
\* Run with TLC:
|
|
\* java -jar tla2tools.jar -config Wave.cfg MC_Wave
|
|
\*
|
|
\* Run with Apalache:
|
|
\* apalache-mc check --config=Wave.cfg MC_Wave.tla
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* SPECIFICATION
|
|
\* --------------------------------------------------------------------------
|
|
|
|
SPECIFICATION Spec
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* CONSTANTS
|
|
\* --------------------------------------------------------------------------
|
|
|
|
CONSTANTS
|
|
N = MC_N
|
|
F = MC_F
|
|
K = MC_K
|
|
AlphaThreshold = MC_AlphaThreshold
|
|
Beta = MC_Beta
|
|
Values = MC_Values
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* STATE CONSTRAINT (bounds state space for tractable checking)
|
|
\* --------------------------------------------------------------------------
|
|
|
|
CONSTRAINT StateConstraint
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* INVARIANTS (checked at every reachable state)
|
|
\* --------------------------------------------------------------------------
|
|
|
|
INVARIANT MC_TypeOK
|
|
INVARIANT MC_Safety
|
|
INVARIANT MC_AgreementOnAccept
|
|
INVARIANT MC_ConfidenceBound
|
|
INVARIANT MC_DecisionConsistency
|
|
INVARIANT MC_PrefMatchesDecision
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* TEMPORAL PROPERTIES
|
|
\* --------------------------------------------------------------------------
|
|
|
|
\* Finalized decisions never change (action property)
|
|
PROPERTY MC_FinalizedStable
|
|
|
|
\* Liveness: every honest validator eventually finalizes.
|
|
\* This will produce counterexamples under nondeterministic scheduling
|
|
\* because roundDir can alternate forever, preventing beta consecutive
|
|
\* same-direction rounds. This is expected -- Snow liveness is probabilistic.
|
|
\* Uncomment to verify the counterexample exists:
|
|
\*
|
|
\* PROPERTY MC_Liveness
|
|
|
|
\* --------------------------------------------------------------------------
|
|
\* SYMMETRY (reduces state space when Values has 2+ elements)
|
|
\* --------------------------------------------------------------------------
|
|
|
|
\* SYMMETRY MC_Symmetry
|