Reference
Technical documentation
The engine repository is the source for implementation details and measured results. These links group its main entry points by task.
Build and use
- Get started
- Build the source and run a checked query.
- Rust embedding
- Use typed terms and solver APIs from Rust.
- Limitations
- Read the supported and unsupported behavior.
- Examples
- Run examples from the engine repository.
Solver
- SMT logic guides
- Plain-English explanations of division names, with worked examples and use cases.
- Supported logics
- Parser, term, solving, model, and evidence support by fragment.
- SMT fragment atlas
- Machine-readable support and measurement records.
- Parity results
- Credited comparisons with cvc5 and Bitwuzla.
- Regression scoreboard
- Generated results across committed corpora.
Proofs and evidence
- Proof stack
- Evidence production, checking, and reconstruction.
- Trust ledger
- Trusted code and route-specific assumptions.
- Lean-core kernel
- Supported kernel terms and current limits.
- Proof certificate cookbook
- Small queries with evidence and checker commands.
Library and Autogenesis
- Fact schema
- The structure of one ledger fact.
- Autogenesis records
- Numbered records of operations, admissions, declines, and replays.
- Formal mathematics curriculum
- The concept graph used to organize the mathematical library.
- North star
- The long-horizon destinations the architecture is built toward. Current status is in the plan.
Project development
- Plan and status
- Current status with a named source for each number, and the next actions.
- Architecture decisions
- Accepted technical decisions and their evidence.
- Testing and validation
- Checks and required host tools.
- Source repository
- Rust crates, scripts, artifacts, and documentation.