TPT-Equinox

TPT-Equinox is the complete autonomous energy and thermal operating system for a lunar city. It is a hard real-time control system, written in #![no_std] Rust, that balances power generation, battery storage, and the physical deployment of mechanical radiators to keep compute and life-support systems from melting or freezing across the Moon's 28-day light/dark cycle.

Why

The Moon has 14 days of +120 °C daylight followed by 14 days of −130 °C darkness. In vacuum there is no air to carry heat away, so thermal management is purely radiative. A software fault that mis-routes power or mis-deploys a radiator can be catastrophic. Equinox is built around three engineering pillars:

1. Radiation tolerance — Triple Modular Redundancy (TMR) voting at the software level so Single Event Upsets (SEUs) cannot silently corrupt critical state.
2. Formal safety — power-routing logic is formally verified with Kani so a bug can never energize mutually-exclusive high-voltage paths.
3. Predictive control — an orbital insolation/shadow model feeds a Model Predictive Control (MPC) loop that smoothly balances loads without brownouts.

Architecture

Equinox is a Cargo workspace of small, #![no_std]-capable crates:

Crate	Responsibility
tpt-equinox-tmr	Generic 3-way voting + scrub-on-mismatch over Copy state
tpt-equinox-power	Circuit/breaker topology + mutually-exclusive routing
tpt-equinox-orbital	Const-generic terrain heightmap, sun-vector math, shadow casting
tpt-equinox-mpc	Const-generic fixed-size LTI MPC prediction + cost optimization
tpt-equinox-thermal	Integrates TMR + orbital + MPC into radiator deployment decisions
tpt-equinox	Umbrella crate with feature-gated re-exports

Firmware skeletons are provided for both supported bare-metal targets:

Firmware	Target	HAL / runtime
tpt-equinox-firmware-stm32	thumbv7em-none-eabihf	stm32f4xx-hal + RTIC
tpt-equinox-firmware-riscv	riscv32imc-unknown-none-elf	riscv-rt + RTIC

High-level data flow

telemetry ──▶ TMR (scrub) ──▶ [orbital: insolation]
                                    │
                                    ▼
                       MPC (predict + optimize) ──▶ radiator/breaker commands
                                    ▲
                       power (safe routing constraint)

Building & testing

Host (desktop) tests run the algorithm crates directly:

cargo test

Cross-compile the firmware for the embedded targets (no std):

cargo build -p tpt-equinox-firmware-stm32 --target thumbv7em-none-eabihf --release
cargo build -p tpt-equinox-firmware-riscv --target riscv32imc-unknown-none-elf --release

Run the formal verification harnesses (requires cargo kani):

cargo kani

Platform note: Kani only ships Linux/macOS release assets (*-unknown-linux-gnu, *-apple-darwin); there is no Windows build. Its proof backend (CBMC/Z3) and bundled rustc are Unix-only, so cargo kani cannot be installed on native Windows PowerShell.

Running Kani locally via WSL

If you want to run the proofs on this Windows machine, use WSL2 (Ubuntu):

wsl --install -d Ubuntu            # one-time
wsl -e bash -lc "cd /mnt/c/Programming/tpt-equinox && \
  TAG=\$(curl -sSL https://api.github.com/repos/model-checking/kani/releases/latest | grep -oP '\"tag_name\":\s*\"\K[^\"]+') && \
  curl -sSL \"https://github.com/model-checking/kani/releases/download/\${TAG}/kani-\${TAG}-x86_64-unknown-linux-gnu.tar.gz\" -o ~/kani.tar.gz && \
  tar -xzf ~/kani.tar.gz -C ~ && \
  export PATH=\"\$HOME/kani/bin:\$PATH\" && \
  cargo kani"

The harnesses live in crates/*/src/kani.rs, compiled only under cfg(kani) (set by cargo kani), so a normal cargo build/test ignores them. CI (.github/workflows/ci.yml, the kani job) installs the official Linux release and runs the proofs on Ubuntu runners.

License

Licensed under either of

• Apache License, Version 2.0 (LICENSE-APACHE)
• MIT license (LICENSE-MIT)

at your option.

Contribution

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.