proofs/formal/lean/lean-toolchain at main

mirror of https://github.com/zooai/proofs.git synced 2026-10-30 14:49:47 +00:00

Files

T

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

1 line

24 B

Plaintext

Raw Permalink Blame History

leanprover/lean4:v4.14.0

1 line 24 B Plaintext Raw Permalink Blame History

1 line

24 B

Plaintext

Raw Permalink Blame History