Status: TRL 4 (Lab Validated)

A small,
checkable
safety gate.

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

2-4µs

Est. per tick, RV32IMC emulator

SMT Solver

CHECKED

Spec + float32 step function

Compliance

NONE

Not assessed (SIL-3 was a target)

Jitter

BOUNDED

144-467 instructions per tick

Universal Specification v2.0

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.

Spatial & Temporal Guard

Targets GNSS spoofing by monitoring spatial divergence. Staleness (replay) checks are part of the language concept but are not implemented in this repository.

Metabolic Energy Reserves

Concept: battery voltage and fuel metrics as invariants. Not implemented in this repository.

Graceful Degradation

Concept: fuzzy zones for graceful degradation. Not implemented in this repository.

UniversalMachineGuard.bio
// 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;
  }
}

The 5-Stage Validation Pipeline

A roadmap that borrows the structure of DO-178C and IEC 61508. No stage is certified; the status of each is stated below.

01

Formal Semantics Proof

02

Tool Qualification & Synthesis

03

Safety Standard Alignment

04

Military Field Validation

05

Operational Assurance Case

Evidence
Stage 1: Partial
Language & Logic Proof

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)

Illustrative scenarios

Hand-drawn illustrations of two failure scenarios. The curves are typed-in example numbers, not measurements or simulation results.

!

Aviation Integrity

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.

Isolation Speed: Illustrative
SHIELD

Logic Response

Example rule triggered (illustration)