# Proofs


Proof examples show how HOAS terms become kernel-checked evidence and
usable Nix values. Start with computational equality, then move to
reusable equality combinators and verified function extraction.

The source for this section lives under [examples/](https://github.com/kleisli-io/nix-effects/tree/main/examples).

## Walkthroughs

- [Proof Basics](/nix-effects/proof-examples/proofBasics): Computational proof examples checked by the HOAS kernel and exposed as ordinary Nix values.
- [Equality Proofs](/nix-effects/proof-examples/equalityProofs): Derive reusable equality combinators from the J eliminator and check them through the kernel.
- [Verified Functions](/nix-effects/proof-examples/verifiedFunctions): Kernel-checked HOAS programs extracted into plain Nix functions.