Falcon V Core — Architecture and Integration Bulletin
1. Executive Summary & The Core Moat (Living GSN vs. Static PDF)
Safety arguments often remain frozen in long PDF safety cases and DOORS traceability matrices while software, neural-planner weights, perception timing, and controller parameters change each sprint. Falcon V addresses the configuration-control problem by maintaining a typed, versioned assurance graph and by recompiling defined checks when bound sources change.
It is a design-time Safety Compiler: it preserves source locations, node and edge revisions, review state, and the exact snapshot used for an assessment. The internal model is a graph, not a collection of copied argument trees. Shared evidence remains shared, and a passing structural profile rejects supported_by cycles.
Mathematical Invariant: Uncertainty operations utilize exact rational intervals over ℚ; missing values remain missing rather than becoming zero. For a snapshot S=(V,E,ρ), V is the set of typed nodes, E the typed relations, and ρ the source and revision bindings.
2. The 4-Pillar Unified Architecture
Pillar 1 — High-Throughput ReqIF & ALM Streaming Pipeline
stream_parser.py incrementally scans and prunes ReqIF XML while enforcing upload, ZIP expansion, compression-ratio, depth, element, object, and relation budgets. Declaration detection rejects DTD and entity syntax across chunks and recognizes UTF-8, UTF-16, and UTF-32 byte signatures before XML parsing.
The pipeline sanitizes embedded XHTML, preserves source identifiers, rejects duplicate or colliding identifiers, and proposes GSN / assume-guarantee roles for engineering review with explicit trust labeling.
Pillar 2 — Formal SMT Safety & Parametric Envelope Compiler
envelope.py represents bounded SI-domain inputs as exact rationals and checks the physical stopping relation:
Feasibility, single-objective candidate checks, and optimum claims are separate results. contracts.py implements a bounded static scalar QF_LRA subset for contracts C = ⟨A, G⟩. It reports source consistency, port/unit compatibility, assumption refinement, and guarantee refinement as separate obligations.
A separate acyclicity.py module queries Z3 for SAT counterexamples or an UNSAT result for support cycles; unknown, invalid input, and runtime failure remain distinct.
Pillar 3 — Autoware ROS 2 Runtime Bridge
autoware.py parses the scoped obstacle_stop_planner.param.yaml profile and checks declared demo thresholds. Changes to max_longitudinal_margin or emergency_stop_acceleration flag proposed Sn-DECEL-LIMIT evidence bindings; latency spikes flag Sn-CAN-LATENCY.
Pillar 4 — Tamper-Evident Cryptographic Audit Ledger & SoD Gate
rbac.py uses SQLite WAL, server-side membership and role state, BEGIN IMMEDIATE, policy-generation compare-and-swap, and one transaction for the state transition plus audit insert. Approval is rejected when the actor is the last editor.
Each audit entry binds the preceding entry and current action with deterministic SHA-256, forming a tamper-evident audit ledger that supports segregation-of-duties (SoD) workflows for ISO 26262 audits.
3. Trust Boundary, Scope & Research Annex
Producer outputs and research reports carry trusted=false. The only positive trusted marker is emitted by src/capa/verifier for a passing scope="graph_structure_only" VerificationReport; it denotes only the named structural checks.
Python, Pydantic, canonicalization code, dependencies, the operating system, and hardware remain trusted assumptions. scripts/check_boundaries.py checks source-level import and trust-marker rules via AST analysis.
4. Deployment & Air-Gap Sovereignty
Falcon V Studio packages a static interface in a Tauri v2 Rust shell and launches a PyInstaller-built Python sidecar. The sidecar binds once to 127.0.0.1 on an operating-system selected port, receives a per-launch session key over stdin, requires it in the X-Falcon-Token header, and stores project data locally.
The desktop CSP blocks remote scripts and frames; the documented runtime path does not need a hosted application server, system Python, Node.js, or a product telemetry component.