docs: make AsciiDoc canonical for CONTRIBUTING/GOVERNANCE/MAINTAINERS

CONTRIBUTING.adoc

@@ -1,20 +1,90 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 = Contributing Guide
+:toc: preamble
+
+Thank you for considering a contribution to Oblíbený.
 
 == Getting Started
 
-1. Fork the repository
-2. Create a feature branch from `main`
-3. Sign off commits (`git commit -s`)
-4. Submit a pull request
+[source,bash]
+----
+git clone https://github.com/hyperpolymath/oblibeny.git
+cd oblibeny
 
-== Commit Guidelines
+just ci      # dune lint + conformance suite + Zig FFI compile-check + escape-hatch guard
+just proofs  # type-check (= prove) the Idris2 ABI layer
+----
 
-* Conventional commits: `type(scope): description`
-* Sign all commits (DCO required)
-* Atomic, focused commits
+Toolchain installation (OCaml 5.1.1 + dune, Idris2 0.7.0, Zig 0.13) is
+documented in link:docs/TOOLCHAIN.adoc[docs/TOOLCHAIN.adoc]; the version
+pins live in `.tool-versions`.
 
-== License
+== Repository Structure
+
+----
+oblibeny/
+├── bin/                 # OCaml executable entry point
+├── lib/                 # OCaml compiler library (lexer, parser, typecheck,
+│                        #   eval, constrained_check, static_analyzer)
+├── test/                # Conformance + unit suite (dune runtest)
+├── src/abi/             # Idris2 ABI proof layer (oblibeny-abi.ipkg;
+│                        #   Packages/, Lang/ metatheory)
+├── ffi/zig/             # Zig crypto FFI (liboqs/libsodium) + obli-pkg
+├── examples/            # .obl programs and packages/hello.zpkg
+├── docs/                # Documentation (TOOLCHAIN, DISTRIBUTION-ARCHITECTURE, …)
+├── deploy/              # Deployment manifests (kubernetes/, svalinn-compose.yaml)
+├── .machine_readable/   # A2ML project metadata (6a2/) + contractiles
+├── .github/workflows/   # CI gates (see ci.yml root-cause note)
+├── justfile             # Task runner — all operations go through this
+├── README.adoc
+├── GOVERNANCE.adoc      # Sole-maintainer governance model
+├── MAINTAINERS.adoc
+├── ROADMAP.adoc
+└── SECURITY.md
+----
+
+== How to Contribute
+
+=== Reporting Bugs
+
+1. Search existing issues first.
+2. Include environment details (OS, toolchain versions from `.tool-versions`),
+   steps to reproduce, and expected vs actual behaviour.
+
+=== Suggesting Features
+
+Check link:ROADMAP.adoc[ROADMAP.adoc] and existing issues first, then open an
+issue with a problem statement, proposed solution, and alternatives considered.
 
-Contributions licensed under project license.
+== Development Workflow
+
+=== Branch Naming
+
+----
+feat/short-description       # New features
+fix/issue-number-description # Bug fixes
+docs/short-description       # Documentation
+test/what-added              # Test additions
+refactor/what-changed        # Code improvements
+security/what-fixed          # Security fixes
+----
+
+=== Commit Messages
+
+We follow https://www.conventionalcommits.org/[Conventional Commits]:
+`type(scope): description`. Sign off commits (`git commit -s`, DCO).
+Keep commits atomic and focused.
+
+=== The Proof Gate
+
+The Idris2 ABI layer is a *proof* layer: CI rejects any soundness escape
+hatch (`believe_me`, `postulate`, `assert_total`, `partial`, `idris_crash`,
+holes) in `src/abi/Crypto.idr` and `src/abi/Packages`. Run the same gate
+locally with `just guard-escape-hatches`; `just ci` includes it. A change
+that only passes by weakening a proof will not merge.
+
+== License
 
+Contributions are licensed under the project licence (see `LICENSE` and the
+SPDX headers each file carries).

README.adoc

@@ -453,7 +453,7 @@ Libraries: liboqs 0.10.0+ and libsodium 1.0.19+
 
 == Contributing
 
-See link:CONTRIBUTING.md[CONTRIBUTING.md] for development guidelines.
+See link:CONTRIBUTING.adoc[CONTRIBUTING.adoc] for development guidelines.
 
 **Code of Conduct**: link:CODE_OF_CONDUCT.md[CODE_OF_CONDUCT.md]
 

docs/learning-paths/README.adoc

@@ -0,0 +1,34 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+= Learning Paths
+:toc: preamble
+
+Audience-divided paths for engaging with Oblíbený beyond setup and a basic
+run. Skeleton for issue #79 — each track below becomes its own page.
+
+== End users — _use the language_
+
+* The dual form: Turing-complete factory → Turing-incomplete constrained
+  form, and why.
+* Writing and running `.obl`; the reversible/accountable constrained form;
+  the `echo[A,B]` residue by example.
+* Reading the accountability trace (`--dump-trace`).
+* `obli-pkg` usage and the triple-signature trust model
+  (Dilithium5 + SPHINCS+ + Ed25519).
+
+== Developers — _extend the language_
+
+* Architecture walkthrough:
+  `lexer → parse → typecheck → eval → constrained_check → static_analyzer`.
+* The proof layer for newcomers: the Idris2 ABI
+  (`installReversible`/`echoResidueNonTrivial`) and the `Lang.*` metatheory
+  (#78) — what each guarantee means, how to extend a slice, the
+  model-fidelity caveat.
+* The Zig crypto FFI; adding a language feature end-to-end.
+
+== Maintainers — _run the project_
+
+* CI gates (`justfile`, `ci.yml`), and the escape-hatch guard discipline.
+* The contractiles + `.machine_readable/6a2/` governance model.
+* The `docs/proof-debt.md` ledger discipline; standards reusable workflows;
+  the release transition.