Technical Documentation

Explore the architectural components, APIs, and formal validation workflows of First Synthesis technologies. This documentation is intended for systems engineers and formal verification researchers.

1. Monist Engine CLI

To run the Monist Engine locally and execute paradox evaluations at hardware speed, utilize the included monist-cli:

# Clone the repository
git clone https://github.com/ryanncode/monist.git
cd monist

# Run the CPU benching suite
cargo bench -p monist-bench-cpu

# Execute a mathematical diagnostic (e.g., Burali-Forti)
cargo run --bin burali_forti

2. NF-Sketches Formal Verification

To rigorously prove that the mathematical bounds executed by Monist are sound, you can pipe the SMT-LIB constraints directly into our Lean 4 formal lab.

Environment Setup

Ensure elan is installed and up-to-date. Clone the companion formal proofs repository as a sibling directory to monist:

git clone https://github.com/ryanncode/nf-sketches.git
cd nf-sketches

Retrieving Dependencies and Building

Fetch the required mathlib dependencies and compile the formal proofs using the Lean 4 Lake package manager:

lake fetch
lake build

Cross-Language Differential Testing

You can automatically pipe the semantic witnesses generated by the Rust Monist Engine directly into the Lean 4 parse-strat interpreter. This proves 1-to-1 equivalence between the geometric bounds of our physical graph execution and our machine-checked theorems.

# From the root of the monist repository:
./scripts/run_differential_tests.sh

For manual piping of specific SMT-LIB blocks:

cd tools/monist-examples
cargo run --bin specker_refutation | awk '/; === BEGIN STRATIFICATION WITNESS ===/{flag=1; print; next} /; === END STRATIFICATION WITNESS ===/{print; flag=0} flag' > out.smt
cd ../../../nf-sketches/parse-strat
lake exe parse-strat --ingest-smt < ../../monist/tools/monist-examples/out.smt

For complete API mappings and architecture graphs, view the Rustdoc API Reference.