The security of a zero-knowledge proof system depends on probability: the chance of anyone successfully cheating must be negligible.
Our formal verification team built Foxglove to make proving these guarantees easier and more scalable.
Foxglove is an open-source framework for reasoning about programs that use randomness in Lean, a language for machine-checked proofs.
Built on Iris-Lean, it provides formally verified rules for reasoning about randomness, independence, and conditioning.
Crucially, Foxglove enables researchers to write reusable specifications: they can verify individual components separately, then combine their guarantees into larger security proofs.
Foxglove integrates with ArkLib, our Lean library for formally verified cryptographic proof systems.
This is increasingly important as Ethereum moves toward bringing zero-knowledge proofs into its base layer, where cryptographic security is critical.
Foxglove builds on Bluebell by Dr. Jialu Bao, Dr. Azadeh Farzan - @AzadehFarzan, and Dr. Emanuele D’Osualdo - @bordaigorl, who also advised the project, and on Amaryllis by Lohse et al.
Funded by an @ethereumfndn grant.
github.com/NethermindEth/…
Our formal verification team built Foxglove to make proving these guarantees easier and more scalable.
Foxglove is an open-source framework for reasoning about programs that use randomness in Lean, a language for machine-checked proofs.
Built on Iris-Lean, it provides formally verified rules for reasoning about randomness, independence, and conditioning.
Crucially, Foxglove enables researchers to write reusable specifications: they can verify individual components separately, then combine their guarantees into larger security proofs.
Foxglove integrates with ArkLib, our Lean library for formally verified cryptographic proof systems.
This is increasingly important as Ethereum moves toward bringing zero-knowledge proofs into its base layer, where cryptographic security is critical.
Foxglove builds on Bluebell by Dr. Jialu Bao, Dr. Azadeh Farzan - @AzadehFarzan, and Dr. Emanuele D’Osualdo - @bordaigorl, who also advised the project, and on Amaryllis by Lohse et al.
Funded by an @ethereumfndn grant.
github.com/NethermindEth/…
