Skip to main content

​
spec show

Show a spec node from a locked spec package: its Op Spec, formula, constants, tensors, shape domain and the number of layers it appears in. --lean also prints the Op Spec’s Lean 4 definition.
The key must name a node (<model>@<version>:<layer-path>), and the model must be locked in the current project. To browse a model without a project, use theformalera-conformance spec <model> or the Spec Hub pages.

​
spec new

Draft a Lean 4 Model Spec from a torch.export program. Engineering nodes (KV cache, device and dtype moves, memory-only views, backend branches) are stripped. Recognised subgraphs become Op Spec instances, and anything else is marked -- REVIEW:. See Write and check a spec. It reports how many graph nodes it read, how many Op Spec instances it produced, how many engineering nodes it stripped, and how many need review:

​
spec check

Check a spec package (a Lake workspace; default .):
  1. lake build: types, dimensions and every proof;
  2. lake env lean Audit.lean, if present: every audited theorem uses only propext, Classical.choice and Quot.sound;
  3. if the theformalera-spec executable is built: for each model, the graph’s inputs are all produced by another node, a graph input or a cache value.
“Unconnected inputs” is a warning, not a failure: a node reads a graph value that no other node produces. In spec 1.0 this happens where a model skips a step: Granite has no q/k norm before RoPE, and Muse Glimmer’s NoPE layers have no RoPE before attention. The value flow then names the skipped step’s output. It does not affect what each node computes; it does affect L3 data-flow matching across those nodes.