Apoth3osis
<_RESEARCH/PROJECTS

Heyting Base Contracts

DEPLOYED0 SORRY5 MENTAT CERTSLean 4 + Solidity
>_VERIFICATION.SEAL
FORMALLY VERIFIED • LEAN 4 • MACHINE-CHECKED • APOTH3OSIS∀∃⊢→∧∨¬≡QED0 SORRY

Formal Verification Certificate

All invariants formally verified in Lean 4. Contracts deployed on Base Sepolia.

0 SORRY

Heyting Base Contracts • Lean 4 + Mathlib • Apoth3osis Labs

❓

The Central Question

Can mathematical proofs be published as on-chain attestations? This project deploys three smart contracts on Coinbase’s Base: a verification oracle that stores proof verification results immutably, NFT audit certificates (ERC-721) representing verified theorems, and ZK credentials enabling privacy-preserving proof of verification status. The contract invariants are themselves formally verified in Lean 4.

Key Verified Results

oracle_consistency

No conflicting attestations for same proof hash

Oracle.lean

certificate_unique

One NFT per verified proof (no duplicates)

Certificate.lean

credential_sound

ZK proofs verify only for valid attestations

Credential.lean

Resources

GHGitHub RepositoryIDXAll Research Projects
← All Research ProjectsGitHub →