Files
proofs/LLM-formal.md
zeekay c86eec94cb merge: absorb /Users/z/work/zoo/formal into proofs (de-duplicate)
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.
2026-05-12 21:13:00 -07:00

35 B

formal — AI Assistant Context