Skip to content

Tools Creative Docs About

Menu

Tools
Creative
Docs
About

theoremc

Formally verified theorems as engineering artefacts. A `theorem_file!` macro expands `.theorem` schemas into compile-time verification modules for Kani.

Introduction

Build discovery

Theorem file loading

Path validation rules
Error variants
Example

Theorem document schema

Loading theorem documents
Top-level fields
Identifier rules
Non-empty constraints
Expression syntax validation
Step and Let binding validation
Subordinate types
Value forms in arguments
Decoded argument types (`ArgValue`)
Examples
Error handling
Minimal example

Declaring action signatures

Action name mangling

Mangling a canonical action name
Mangling algorithm
Building-block functions
Injectivity guarantee

Mangled-identifier collision detection

What is checked
Calling the check directly

Per-file module naming

Path mangling functions
Composite entry point
Collision resistance

Theorem harness naming

Harness naming helpers
Duplicate theorem-key rejection

Source

Source material

Contents

Introduction
- Introduction
Build discovery
- Build discovery
Theorem file loading
Theorem document schema
Declaring action signatures
- Declaring action signatures
Action name mangling
Mangled-identifier collision detection
Per-file module naming
Theorem harness naming

Introduction

Updated Jul 16, 2026

This guide covers the behaviour and application programming interface (API) of the theoremc library from the perspective of a library consumer.

df12 Productions

Serious systems, playful worlds. We ship tools that cut build times and stories that map the human edge of complex networks.

OSS & Licences

Limela — licence
Netsuke — licence
mxd — licence
Episodic — licence

Stay in touch

[email protected]
GitHub
Bluesky

Built for curious builders and storytellers everywhere. © 2026 df12 Productions.