import { Callout } from 'nextra/components'
import { VerityHero } from '../components/VerityHero'
import { CodeCompare } from '../components/CodeCompare'
import { ReportCallout } from '../components/ReportCallout'

<VerityHero />

<CodeCompare />

<ReportCallout title="Where the trust comes from">
A small, audited Lean EDSL with example contracts that compile to EVM artifacts.
Every claim is machine-checked and every assumption is documented. Compilation
correctness rides on `Compiler/Proofs/IRGeneration/Contract.lean` (generic
whole-contract `CompilationModel -> IR` theorem for the current supported
fragment), no per-contract bridge axioms. The full three-layer breakdown lives
on the [Trust Model](/trust-model) page; the live theorem inventory is on
[Verification Status](/verification).
</ReportCallout>

## The Three-Layer Structure

Every contract is three things at once: a **specification** of what it should do,
an **implementation** that runs, and a **proof** that ties them together.

### Specification &nbsp;·&nbsp; *what should be true*

```verity
def mint_spec (to : Address) (amount : Uint256) (s s' : ContractState) : Prop :=
  s'.storageMap 1 to = add (s.storageMap 1 to) amount ∧
  s'.storage 2 = add (s.storage 2) amount ∧
  storageMapUnchangedExceptKeyAtSlot 1 to s s' ∧
  sameContext s s'
```

### Implementation &nbsp;·&nbsp; *what runs on chain*

```verity
def mint (to : Address) (amount : Uint256) : Contract Unit := do
  onlyOwner
  let currentBalance ← getMapping balances to
  let newBalance ← requireSomeUint (safeAdd currentBalance amount) "Balance overflow"
  let currentSupply ← getStorage totalSupply
  let newSupply ← requireSomeUint (safeAdd currentSupply amount) "Supply overflow"
  setMapping balances to newBalance
  setStorage totalSupply newSupply
```

### Proof &nbsp;·&nbsp; *they agree*

```verity
theorem mint_meets_spec (s : ContractState) (to : Address) (amount : Uint256)
  (h_owner : s.sender = s.storageAddr 0) :
  let s' := ((mint to amount).run s).snd
  mint_spec to amount s s' := by
  simp only [mint, onlyOwner, getMapping, setMapping]
  simp [h_owner]
```

Lean checks every proof at compile time. A broken proof is a broken build.

## Read next

import { ReadingList } from '../components/ReadingList'

<ReadingList items={[
  { href: '/architecture', title: 'Architecture Overview', note: 'One screen: EDSL → CompilationModel → IR → Yul → EVM.' },
  { href: '/getting-started', title: 'Getting Started', note: 'Local setup and your first verification run.' },
  { href: '/first-contract', title: 'Your First Contract', note: 'A guided spec-to-proof walkthrough.' },
  { href: '/trust-model', title: 'Trust Model', note: 'What is verified, what is trusted, and the Layer 1/2/3 framing.' },
  { href: '/verification', title: 'Verification Status', note: 'Theorem inventory and proof status.' },
  { href: '/faq', title: 'FAQ', note: 'Why Lean, why an EDSL, how Verity compares to other formal-methods tools.' },
]} />

<Callout type="info">
**For agents and tooling:** see [/llms.txt](/llms.txt), or add `.md` to any
page URL for raw markdown.
</Callout>

Verity is a research project by [LFG Labs](https://lfglabs.dev).