docs+feat: honest wiki claims + Dense pair/keyword constructor so docs resolve (#68)

## Summary

A **documentation-honesty pass** on the flagship wiki (from a dedicated
doc-vs-code audit), plus the one **code change** needed to make the
wiki's own examples valid — fixing at source rather than sweeping the
symptom.

Every claim below was ground-truthed against the code and the repo's own
benchmark, *not* taken on the audit's word (some audit findings were
over-flagged — see "What the audit got wrong").

## Docs — no overclaim

| Claim (before) | Reality | Fix |
|---|---|---|
| "2-3× faster than PyTorch" (FAQ/Vision/Migration/Home) | The repo's
**own** benchmark measures a **~0.73× geomean** vs PyTorch — slower on
average, winning 11/25 ops; PyTorch's MKL wins large element-wise ops
5–25× | State the measured truth, link
`benchmark/results_2026-02-20_framework-comparison.md`, and say the
differentiator is provable correctness (the benchmark's own conclusion)
|
| "Rust backend" as the current/optional compute backend | The compute
backend is **Zig** (`ZigBackend`); there is **no** `RustBackend` compute
path (the only `RustBackend` is in vendored
`AcceleratorGateVendored.jl`) | Fix present-tense mislabels → Zig |
| `compile(model, backend=:rust/:zig/:julia)` | `compile(;
backend::AbstractBackend = JuliaBackend())` — a **symbol** MethodErrors
| → `backend=ZigBackend("/path/to/libaxiom_zig.so")` (the README's real
idiom) |
| "`@ensure`/`@prove` are PROVEN, not just tested" / "mathematical
proof" | `prove.jl` itself says its heuristics are "**NOT** symbolic
execution and **NOT** formal verification" and returns `:unknown`
honestly | Soften to match the code's own disclaimer |
| `[Rust Backend](Rust-Backend.md)` | File does not exist | →
`Performance-Tuning.md` (real page) |

## Code — make the documented API real (doctrine: fix at source)

The docstring (`src/layers/dense.jl:38`) and **dozens** of wiki examples
use Flux-style `Dense(in => out)` and keyword `activation=…`, but the
constructor was positional-only — so those standalone examples
MethodError. Rather than sweep 40+ doc sites, the constructor now
accepts what its own docs advertise:

- `Dense(in => out)`, `Dense(in => out, relu)`, `Dense(in => out;
activation=relu)` (Flux-style pair form)
- `Dense(in, out; activation=relu)` (keyword activation)
- Positional `Dense(in, out, relu)` still works and behaves
**identically**; the keyword wins if both are given.

Verified: **0 method ambiguities** (`detect_ambiguities(Axiom;
recursive=true) == 0`), forward pass unchanged, new-forms guarded in the
`Dense Layer` testset (**11/11 pass**), and the two disagreeing Dense
docstrings reconciled.

## What the audit got wrong (and I corrected for)

- The audit claimed *all* `Dense(=>)` examples MethodError. In fact,
**inside `@axiom` blocks the macro parses layers structurally and
accepts both pair-form and keyword-activation** — so the Tutorials build
fine. Only **standalone** constructor calls were broken. This
constructor change makes both paths correct.

## ⚠️ Two items I deliberately did NOT change — they need your decision

1. **Version maturity contradiction.** `Project.toml` / `src/Axiom.jl` /
the benchmark all say **1.0.0**, but `FAQ.md:30` says "alpha (v0.1.0)"
and the README roadmap leaves "v1.0 — production ready" **unchecked**.
Resolving this is a release-semantics call (bump docs to 1.0, or the tag
down to 0.1) — flagged, not touched.
2. **Roadmap "Rust backend" vs shipped Zig.** The forward-looking
roadmap (`Vision.md` "The Road Ahead", `Roadmap-Commitments.md` — which
declares itself the source of truth — and `Certification-Readiness.md`)
commits to a *future* "Full Rust backend", and
`Roadmap-Commitments.md:94` cites a non-existent
`docs/wiki/Rust-Backend.md`. The **shipped** backend is Zig, and estate
policy migrated Rust→Zig. I did **not** rewrite the commitments doc
(outward-facing promise; intent is yours). Please decide: align the
roadmap to Zig, or keep a genuine Rust-backend commitment (and add the
missing `Rust-Backend.md`)?

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_01UPFC9YQ7g9gc3VnRox42Q1

---
_Generated by [Claude
Code](https://claude.ai/code/session_01UPFC9YQ7g9gc3VnRox42Q1)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

docs/wiki/FAQ.md

@@ -226,14 +226,19 @@ end
 
 ### Is Axiom.jl faster than PyTorch?
 
-**Inference**: Yes, 2-3x faster with Zig backend
-**Training**: Comparable (Julia) to 1.5x faster (Zig)
+**It depends on the operation.** Axiom's own measured benchmark
+(`benchmark/results_2026-02-20_framework-comparison.md`) records a geometric mean of
+~0.73× PyTorch for the SmartBackend — i.e. slower on average, winning 11 of 25 ops.
+It is faster on small inputs and on RMSNorm/LayerNorm/BatchNorm at small sizes, but
+PyTorch's MKL wins large element-wise ops (sigmoid/gelu/softmax at ≥100K) by 5–25×.
+Axiom's differentiator is provable correctness, not raw speed. Training throughput is
+not separately benchmarked.
 
 ### How do I enable the Zig backend?
 
 ```julia
 # Compile for Zig
-model = compile(my_model, backend=:zig)
+model = compile(my_model, backend=ZigBackend("/path/to/libaxiom_zig.so"))
 
 # Or set environment variable
 ENV["AXIOM_BACKEND"] = "zig"

docs/wiki/Framework-Comparison.md

@@ -21,14 +21,14 @@
 
 ```julia
 # The type system ensures correctness
-model = @axiom begin
+model = @axiom MnistNet begin
     @ensure input_shape == (784,) "MNIST images must be 784-dim"
     Dense(784 => 256, activation=relu)
     Dense(256 => 10, activation=softmax)
     @ensure output_shape == (10,) "Must output 10 classes"
 end
 
-# Compile-time verification
+# Verification (static where a property is provable; runtime otherwise)
 @prove BoundedOutputs(0.0, 1.0) model
 ```
 

docs/wiki/Home.md

@@ -126,9 +126,9 @@ result = verify(model, properties=[ValidProbabilities(), FiniteOutput()], data=b
 
 ## Optional Backends
 
-Axiom is Julia-first. The Rust backend is optional and used only when you
-explicitly enable it (e.g., for high-performance kernels or SMT runner
-hardening). Most users can ignore it entirely.
+Axiom is Julia-first. The optional **Zig backend** provides native SIMD kernels for
+high-performance hot paths and is used only when you explicitly enable it
+(e.g. `compile(model, backend=ZigBackend(path))`). Most users can ignore it entirely.
 
 ---
 
@@ -139,10 +139,14 @@ hardening). Most users can ignore it entirely.
 | Shape checking | Runtime | Runtime | **Compile time** |
 | Formal proofs | No | No | **Yes** |
 | REPL exploration | No | No | **Yes** |
-| Performance | Good | Good | **Better** (Rust) |
+| Performance | Good | Good | Competitive (Zig)† |
 | Safety certification | No | No | **Yes** |
 | Learning curve | Low | Medium | Low |
 
+> † *Performance is workload-dependent: Axiom's Zig SmartBackend is competitive with
+> PyTorch on small/medium ops and behind on large element-wise ops (geomean ~0.73×).
+> See `benchmark/results_2026-02-20_framework-comparison.md`.*
+
 ---
 
 ## Documentation Map
@@ -160,7 +164,7 @@ hardening). Most users can ignore it entirely.
 - [@axiom DSL](Axiom-DSL.md) - The declarative model definition
 - [Verification System](Verification.md) - @ensure and @prove
 - [Architecture](Architecture.md) - Deep dive into design
-- [Rust Backend](Rust-Backend.md) - Performance architecture
+- [Performance Tuning](Performance-Tuning.md) - Backend selection and optimization
 
 ### API Reference
 - [Complete API Reference](API-Reference.md) - All functions, types, macros

docs/wiki/Migration-Guide.md

@@ -11,10 +11,15 @@
 |--------------|---------|----------|
 | Compile-time shape checking | | |
 | Formal verification | | |
-| 2-3x faster inference | | |
+| Competitive kernel performance† | | |
 | REPL exploration | | |
 | Keep existing models | | |
 
+> † *Performance is workload-dependent — Axiom is competitive with PyTorch on
+> small/medium ops and behind on large element-wise ops; see
+> `benchmark/results_2026-02-20_framework-comparison.md`. The real differentiator is
+> compile-time verification, not raw speed.*
+
 **The best part**: You don't have to rewrite anything. Import and go.
 
 ---
@@ -460,12 +465,13 @@ After migration, you can compile for production:
 # Development (Julia backend)
 dev_model = from_pytorch("model.pytorch.json")
 
-# Production (Zig backend) - 2-3x faster
-prod_model = compile(dev_model, backend=:zig, optimize=:aggressive)
+# Production (Zig backend)
+prod_model = compile(dev_model, backend=ZigBackend("/path/to/libaxiom_zig.so"), optimize=:aggressive)
 
-# Benchmark
-@time dev_model(test_input)   # 0.012s
-@time prod_model(test_input)  # 0.004s
+# Benchmark on your own workload — op-level medians are in
+# benchmark/results_2026-02-20_framework-comparison.md
+@time dev_model(test_input)
+@time prod_model(test_input)
 ```
 
 ---

docs/wiki/Vision.md

@@ -100,31 +100,35 @@ Flatten()(input) |> Dense(784, 10)  # ✓ Compiles
 
     # ... layers ...
 
-    # These are PROVEN, not just tested
+    # @ensure adds runtime contracts; @prove attempts to discharge them statically
     @ensure sum(output) ≈ 1.0
     @ensure all(output .>= 0)
     @prove ∀x. no_nan(output(x))
 end
 ```
 
-**What this means**: You get mathematical proof that your model has certain properties.
+**What this means**: `@ensure` attaches runtime contracts that are checked on every
+forward pass; `@prove` attempts to discharge a property *statically* — via
+known-pattern heuristics, or an SMT solver when `SMTLib.jl` is loaded — and honestly
+returns `:unknown` when it cannot. It is not a blanket claim that every property is
+formally proved.
 
 ### 3. Production Performance
 
 ```julia
 # Development: Julia backend (fast iteration)
-model = compile(MyModel, backend=:julia)
+model = compile(MyModel, backend=JuliaBackend())
 
-# Production: Rust backend (maximum speed)
-model = compile(MyModel, backend=:rust, optimize=:aggressive)
-# 2-3x faster than PyTorch, with formal guarantees
+# Production: Zig backend (native SIMD kernels)
+model = compile(MyModel, backend=ZigBackend("/path/to/libaxiom_zig.so"), optimize=:aggressive)
+# Competitive with PyTorch on small/medium workloads — see benchmark/ for measured medians
 ```
 
-**What this means**: No compromise between safety and speed.
+**What this means**: verification guarantees without giving up competitive performance.
 
 ---
 
-## Why Julia + Rust?
+## Why Julia + Zig?
 
 ### Why Not Pure Python?
 
@@ -138,9 +142,9 @@ def broken(x):
 # Only crashes at runtime, maybe
 ```
 
-### Why Not Pure Rust?
+### Why Not a Pure Systems Language?
 
-Rust is great for systems programming. But ML research needs:
+Systems languages like Zig are great for native kernels. But ML research needs:
 
 - **REPL exploration** - Try ideas instantly
 - **Interactive visualization** - Plot results immediately
@@ -156,7 +160,7 @@ Rust is great for systems programming. But ML research needs:
 // This is a flow killer for research
 ```
 
-### Why Julia + Rust?
+### Why Julia + Zig?
 
 **Julia for research**:
 ```julia
@@ -167,11 +171,11 @@ julia> model(randn(4, 10))  # Instant feedback
  ...
 ```
 
-**Rust for production**:
+**Zig for production**:
 ```julia
 # When you're done experimenting
-production_model = compile(model, backend=:rust)
-# Single binary, 2-3x faster, memory safe
+production_model = compile(model, backend=ZigBackend("/path/to/libaxiom_zig.so"))
+# Native SIMD kernels; competitive on small/medium ops (see benchmark/)
 ```
 
 **Best of both worlds.**
@@ -206,7 +210,7 @@ end
 ```julia
 @axiom Model begin
     # ...
-    @prove ∀x. sum(softmax(x)) == 1.0  # Proven mathematically
+    @prove ∀x. sum(softmax(x)) == 1.0  # discharged via @prove (known pattern; SMT when SMTLib.jl loaded)
     @prove ∀x ε. (ε < δ) ⟹ stable(f(x), f(x+ε))  # Robustness
 end
 ```

src/layers/dense.jl

@@ -56,6 +56,9 @@ dense1 = Dense(784, 128)
 # A layer with ReLU activation
 dense2 = Dense(128, 64, relu)
 
+# Flux-style pair form (equivalent), with a keyword activation
+dense2b = Dense(128 => 64, activation=relu)
+
 # A layer without a bias term
 dense3 = Dense(64, 10, bias=false)
 
@@ -72,25 +75,24 @@ mutable struct Dense{T, F} <: AbstractLayer
 end
 
 """
-    Dense(
-        in_features::Int,
-        out_features::Int,
-        activation::F = identity;
-        bias::Bool = true,
-        init::AbstractInitializer = DEFAULT_WEIGHT_INIT,
-        bias_init::AbstractInitializer = DEFAULT_BIAS_INIT,
-        dtype::Type{T} = Float32
-    ) where {T, F}
+    Dense(in_features, out_features, σ = identity; activation = nothing, bias = true,
+          init = GlorotUniform(), bias_init = Zeros(), dtype = Float32)
+    Dense(in_features => out_features, σ = identity; kwargs...)   # Flux-style pair form
 
-Constructs a `Dense` layer.
+Constructs a `Dense` layer. The activation may be supplied positionally (`σ`,
+Flux-style) or via the `activation` keyword (the keyword wins if both are given).
+The pair form `in => out` forwards to the positional constructor, so the
+`Dense(784 => 256)` idiom used throughout the docs resolves to a real method.
 
 Arguments:
 - `in_features::Int`: The number of input features this layer expects. Must be positive.
 - `out_features::Int`: The number of output features this layer produces. Must be positive.
-- `activation::F`: The activation function to apply after the linear transformation.
-                   Can be any Julia function or callable object. Defaults to `identity`.
+- `σ`: The activation function to apply after the linear transformation (positional).
+       Can be any Julia function or callable object. Defaults to `identity`.
 
 Keyword Arguments:
+- `activation`: Alternative to the positional `σ`; overrides it when given. Lets you
+                write `Dense(in, out; activation=relu)` and `Dense(in => out; activation=relu)`.
 - `bias::Bool`: If `true`, a bias term `b` is added to the output. Defaults to `true`.
 - `init::AbstractInitializer`: The initializer strategy for the `weight` matrix.
                                Defaults to `DEFAULT_WEIGHT_INIT` (GlorotUniform).
@@ -108,21 +110,33 @@ Throws:
 function Dense(
     in_features::Int,
     out_features::Int,
-    activation::F = identity;
+    σ = identity;
+    activation = nothing,
     bias::Bool = true,
     init::AbstractInitializer = DEFAULT_WEIGHT_INIT,
     bias_init::AbstractInitializer = DEFAULT_BIAS_INIT,
     dtype::Type{T} = Float32
-) where {T, F}
+) where {T}
     @assert in_features > 0 "in_features must be positive."
     @assert out_features > 0 "out_features must be positive."
 
+    # The activation may be supplied positionally (`σ`, Flux-style) or by the
+    # `activation` keyword (as the docstring and docs advertise); the keyword
+    # wins when both are given.
+    act = activation === nothing ? σ : activation
+
     weight = T.(init(in_features, out_features)) # Initializes as (in_features, out_features) matrix
     b = bias ? T.(bias_init(out_features)) : nothing # Initializes as (out_features,) vector
 
-    Dense{T, F}(weight, b, activation, in_features, out_features)
+    Dense{T, typeof(act)}(weight, b, act, in_features, out_features)
 end
 
+# Flux-style pair form: `Dense(in => out)`, `Dense(in => out, relu)`,
+# `Dense(in => out; activation=relu)`. Forwards to the primary constructor so the
+# `in => out` idiom used throughout the docs resolves to a real method.
+Dense(dims::Pair{<:Integer, <:Integer}, args...; kwargs...) =
+    Dense(Int(first(dims)), Int(last(dims)), args...; kwargs...)
+
 # forward(d::Dense, x::AbstractTensor) is defined in backends/abstract.jl
 # with backend-aware dispatch (routes through Zig/GPU when active).
 

test/runtests.jl

@@ -43,6 +43,19 @@ using JSON
         y = layer_relu(x)
         @test all(y.data .>= 0)  # ReLU output
 
+        # Flux-style pair form: Dense(in => out) — the idiom used throughout the docs.
+        layer_pair = Dense(784 => 128)
+        @test layer_pair.in_features == 784
+        @test layer_pair.out_features == 128
+        @test layer_pair.activation === identity
+        @test size(layer_pair(x)) == (32, 128)
+
+        # activation supplied positionally, by keyword, and via the pair form — all agree.
+        @test Dense(784, 128, activation=relu).activation === relu
+        @test Dense(784 => 128, relu).activation === relu
+        @test Dense(784 => 128, activation=relu).activation === relu
+        @test Dense(784 => 128, bias=false).bias === nothing
+
         # Test shape mismatch
         x_wrong_shape = Tensor(randn(Float32, 32, 783)) # Wrong number of features
         # Note: The actual error will be a MethodError because the matrix multiplication