Skip to content

Formal verification of core circuits (soundness/completeness properties) #945

Description

@joelpeace48-cell

Epic: ZK & Privacy (expansion)

Summary

Attempt formal verification of the claim/nullifier circuits for soundness and completeness.

Background & Problem

Formal guarantees on circuits are the gold standard and a strong grant differentiator.

Acceptance Criteria

  • Key circuit properties formally stated.
  • At least one property machine-checked.
  • Findings documented.

Filed as part of the mainnet-readiness & world-class roadmap. Scope is intentionally small enough for one focused PR; comment to claim.

Metadata

Metadata

Assignees

Labels

Maybe RewardedIssue may be eligible for a GrantFox rewardStellar WaveIssues in the Stellar wave programcryptographyCryptographic primitives & protocolsdifficulty: expertDeep expertise, 2+ weeksformal-verificationKani/SMT formal verificationpriority: lowNice to havetype: researchInvestigation or design spikezkZero-knowledge proofs & privacy

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions