MetaSpace.bio is a specification language and tool chain for small safety gates. This prototype checks GNSS/INS divergence and RF power, with the rule checked by a solver and the generated code measured in an emulator.
Latency
Est. per tick, RV32IMC emulator
SMT Solver
Spec + float32 step function
Compliance
Not assessed (SIL-3 was a target)
Jitter
144-467 instructions per tick
A language showcase. The tools in this repository implement the subset used by examples/drone_shield_v2.bio; the constructs below that go beyond it are not implemented here.
Targets GNSS spoofing by monitoring spatial divergence. Staleness (replay) checks are part of the language concept but are not implemented in this repository.
Concept: battery voltage and fuel metrics as invariants. Not implemented in this repository.
Concept: fuzzy zones for graceful degradation. Not implemented in this repository.
// MetaSpace Universal Specification v2.0 CELL UniversalMachineGuard { INTERFACE { INPUT gps_pos, ins_pos: VECTOR2D; INPUT battery_voltage: FLOAT; INPUT last_packet: TIMESTAMP; } INVARIANTS { // 1. Spatial Continuity (Anti-Spoofing) RULE spatial_integrity: DISTANCE(gps_pos, ins_pos) <= 50.0; // 2. Temporal Freshness (Anti-Jitter) RULE temporal_integrity: STALENESS(last_packet) < 0.1s; // 3. Metabolic Law (Energy Reserve) RULE battery_integrity: battery_voltage > 11.2; } FUZZY_LOGIC { // Deterministic Heuristic: Graceful performance scaling ZONE range_warning: IF battery_voltage < 11.5 THEN MAX_THRUST = 0.5; } STATES { STATE Operational { lock = 0; } STATE ShieldEngaged TYPE SAFETY_LOCK { lock = 1; } TRANSITION FROM Operational TO ShieldEngaged IF spatial_integrity == FALSE OR battery_integrity == FALSE; } }
A roadmap that borrows the structure of DO-178C and IEC 61508. No stage is certified; the status of each is stated below.
A parser and reference semantics exist for a subset of .bio. Z3 checks the invariants of the example against its state machine and proves properties of the float32 step function. No full formal semantics, no MC/DC coverage measurement.
Tool output (results/*.txt)
[FOUND] drone_shield_v1.bio: rf_integrity violated in state Normal
[PROVED] drone_shield_v2.bio: both rules, transition-first semantics
[PROVED] float32: NaN / inf input raises the alarm (F1a, F1b, F4)
[MEASURED] 0 / 100803 mismatches (RISC-V gate vs float32 model)
[MEASURED] 144 / 348 / 467 instructions per tick (min / median / max)
Hand-drawn illustrations of two failure scenarios. The curves are typed-in example numbers, not measurements or simulation results.
Illustration of the AF447 Pitot icing event: a divergence rule between redundant sensors flags the disagreement. Example data only; the AF447 example is not covered by the tools in this repository.
Logic Response
Example rule triggered (illustration)