kaptan/firmware/verification.toml

format = 1

[miri]
toolchain = "nightly-2026-06-23"
target = "x86_64-unknown-linux-gnu"
packages = ["kaptan-spi", "kaptan-err-reportable", "kaptan-log"]
seeds = [0, 1, 2, 3, 4, 5, 6, 7]
flags = [
  "-Zmiri-strict-provenance",
  "-Zmiri-symbolic-alignment-check",
  "-Zmiri-preemption-rate=1",
]
claim = "Existing unit tests and bounded concurrent ownership tests execute with provenance, aliasing, validity and race checks enabled."
limits = "Executed schedules only. Host memory stands in for DMA. No device quiescence, interrupt or MMIO claim."

[kani]
version = "0.68.0"
toolchain = "nightly-2026-08-21"
target = "x86_64-unknown-linux-gnu"
solver = "cadical"
harness_timeout_seconds = 300

[[properties]]
id = "math.sqrt-domain"
package = "kaptan-math"
source = "libs/kaptan-math/src/kani_proofs.rs"
harnesses = ["kani_proofs::sqrt_preserves_domain_and_zero_sign"]
covers = [6]
claim = "All f32 input bit patterns obey square-root domain classification and preserve signed zero. Positive finite inputs return positive finite values."
assumptions = "Kani's floating-point arithmetic model; actual four-iteration implementation, with unwind bound 5."
limits = "No accuracy bound, normalization proof or target floating-point equivalence."

[[properties]]
id = "control.pid-state"
package = "kaptan-control"
source = "libs/kaptan-control/src/kani_proofs.rs"
harnesses = [
  "kani_proofs::pid_constructor_establishes_invariant",
  "kani_proofs::pid_update_preserves_bounds_or_state",
]
covers = [3, 3]
intermediate_nan_line = 196
claim = "The constructor establishes the PID invariant. One update returns finite bounded output and integral, or retains the complete previous state on error. Reset establishes zero integral."
assumptions = "Validated arbitrary configuration and any finite prior integral within its configured bound. Dynamic inputs span all f32 bit patterns."
limits = "Raw Kani reports Failure for one reviewed intermediate-NaN diagnostic at the declared location. Contract assertions and covers pass; the implementation rejects that NaN before state mutation. No tracking-performance, vehicle-stability or complete controller proof."

[[properties]]
id = "safety.commit-authority"
package = "kaptan-safety"
source = "libs/kaptan-safety/src/kani_proofs.rs"
harnesses = [
  "kani_proofs::commit_requires_current_health_and_completed_dwell",
  "kani_proofs::failed_commit_preserves_error_and_latches_inhibition",
  "kani_proofs::clock_regression_requires_successful_inhibited_reset",
]
covers = [4, 1, 2]
claim = "Named public-operation histories check health and dwell before commit, preserve commit errors, latch inhibition, and require successful inhibition to reset a regressed clock."
assumptions = "Positive dwell, arbitrary u64 times and health flags. Callbacks return normally. Each harness declares its finite operation history."
limits = "No arbitrary-history, complete flight-runtime or physical-output proof."

[[properties]]
id = "actuator.dshot-format"
package = "kaptan-actuator"
source = "libs/kaptan-actuator/src/kani_proofs.rs"
harnesses = [
  "kani_proofs::dshot_frame_preserves_payload_and_checksum",
  "kani_proofs::dshot_symbols_round_trip_and_end_low",
  "kani_proofs::dshot_timer_rounding_keeps_compares_inside_period",
  "kani_proofs::arming_duration_product",
  "kani_proofs::arming_frame_count",
]
covers = [3, 2, 2, 2, 3]
claim = "Packet payload/checksum, MSB-first symbol encoding, trailing low symbols and timer rounding satisfy their integer contracts. Arming counts compose a bounded duration/cadence product with a separately proved minimum-frame conversion."
assumptions = "Supported DShot rates and constructor-admitted throttle values. Timer clocks, durations and dispatch cadences span their complete integer types; duration construction admits 1..=8,000 ms. Frame conversion spans all u64 products; frames_at composition is source-reviewed."
limits = "This reference crate is not linked to a physical actuator route. No electrical or execution-timing claim."

# Every workspace package must belong to exactly one area. New owners require
# an explicit account of their evidence and outstanding obligations.
[[areas]]
name = "Numerical core"
packages = ["kaptan-math", "kaptan-navigation", "kaptan-control"]
checks = ["host", "coverage", "targets"]
gap = "Independent numerical tests and strict coverage remain necessary. Complete estimator correctness, error enclosures and target floating-point behavior are not formally established."

[[areas]]
name = "Flight authority"
packages = ["kaptan-safety", "kaptan-flight-runtime"]
checks = ["host", "coverage", "targets"]
gap = "Named safety proofs do not cover every runtime history, mission requirement or physical output consumer."

[[areas]]
name = "Actuator reference"
packages = ["kaptan-actuator"]
checks = ["host", "coverage"]
gap = "No composed physical actuator route or vehicle qualification."

[[areas]]
name = "Unsafe library ownership"
packages = ["kaptan-spi", "kaptan-log", "kaptan-err-reportable"]
checks = ["host", "coverage", "miri"]
gap = "Miri explores finitely many executions. Actual DMA completion and interrupt interference remain hardware obligations."

[[areas]]
name = "Configuration"
packages = [
  "kaptan-config",
  "kaptan-config-derive",
  "kaptan-flight-config",
  "kaptan-ports",
]
checks = ["host", "coverage"]
gap = "Schema compiler fixtures, runtime validation and journal tests do not constitute exhaustive parser or physical power-loss proofs."

[[areas]]
name = "Drivers and observations"
packages = ["kaptan-drivers", "kaptan-sensor", "kaptan-i2c", "kaptan-time"]
checks = ["host", "coverage"]
gap = "Mock bus tests do not establish sensor accuracy, wiring, timing, freshness or recovery on silicon."

[[areas]]
name = "Communication"
packages = [
  "kaptan-mavlink",
  "kaptan-file-mavlink",
  "kaptan-diagnostics-mavlink",
  "kaptan-data-channel",
  "kaptan-tx",
]
checks = ["host", "coverage"]
gap = "Protocol and queue tests do not exhaust every hostile input, transport failure or interleaving."

[[areas]]
name = "Compiler-generated error identities"
packages = ["kaptan-err-reportable-macros"]
checks = ["host", "coverage"]
gap = "Compiler fixtures and final-link checks cover named cases. Runtime-harness coverage does not measure macro expansion coverage."

[[areas]]
name = "MCU platform"
packages = ["platform-stm32f7"]
checks = ["host", "coverage", "targets", "boards"]
gap = "USB wait deadlines and terminal faults have host regression checks. MMIO, assembly, caches, DMA quiescence, interrupt timing, WCET and peak stack remain outside host proof and interpreter evidence."

[[areas]]
name = "Board images"
packages = ["kaptan-geprc-f722-v2", "kaptan-kakute-f7-mini-v3"]
checks = ["targets", "boards"]
gap = "Linked ELF placement checks and image hashes do not qualify physical hardware or flight."

[[areas]]
name = "Configurator"
packages = ["kaptan-configurator"]
checks = ["host", "coverage", "targets"]
gap = "Hosted serial/HTTP and browser-state tests are not exhaustive OS, UI or security verification."

[[components]]
name = "Ground suite"
path = "ground_suite"
checks = ["host: native UTF conversion helper"]
gap = "Flutter/native product builds and operational behavior need their separate documented platform gates."

[[components]]
name = "Build scripts and documentation"
path = "."
checks = ["host: formatting, script tests, API documentation and mdBook"]
gap = "The evidence runner and tools remain trusted software requiring review. No tool qualification or certification credit is asserted."