Safety-Critical Software Engineer, Rust and Ada SPARK

The role

AeroBrain is the SkyDynamics set of high-assurance AI technologies for aerospace and defence. Its parts exchange data through protocols that must behave the same way every time: between the layers of the software, between nodes of the LLiDA database, and between the aircraft, the edge device and the ground.

You design those protocols and write the software that implements them, in the languages chosen for assurance: Rust, Ada SPARK and C++. Where a property can be proved, you prove it; where it cannot, you test it and keep the evidence.

What you will do

• Specify communication and synchronisation protocols: messages, states, timing and behaviour on failure.
• Implement them in Rust, Ada SPARK and C++, with memory safety and bounded use of time and memory.
• Prove the properties that matter (absence of run-time errors, protocol invariants) with SPARK proof and other static analysis.
• Work to safety-critical coding rules and to the objectives of DO-178C: requirements, design, code and tests traced to each other.
• Define the interfaces between languages (Rust, Ada, C and C++) so that guarantees are not lost at the boundary.
• Build the test benches: unit, integration, fault injection and structural coverage.
• Review code and designs, and keep the record a certification authority would ask for.

What you bring

• 8 or more years of professional experience in software for safety-critical or mission-critical systems.
• Strong Rust, including unsafe code, no_std and embedded targets.
• Ada and SPARK: contracts, proof of absence of run-time errors, and the Ravenscar or Jorvik profiles.
• Strong modern C++ under a restricted subset, such as MISRA C++ or AUTOSAR C++14.
• Protocol design and implementation: state machines, serialisation, timing, and behaviour under loss and reordering.
• Familiarity with DO-178C and its supplements, and with MISRA C.
• Experience in aviation, defence, space, automotive, rail or medical devices.
• Master's degree in computer science, electrical or computer engineering, mathematics, physics or a related field.
• Greek, fluent (required).
• English, fluent (required).

Advantages

• A PhD in software engineering, formal methods, programming languages or a related field.
• Formal specification and model checking: TLA+, Event-B, Frama-C or similar.
• DO-333 (formal methods) and DO-330 (tool qualification).
• Real-time operating systems and ARINC 653 partitioning.
• Avionics data buses: ARINC 429, ARINC 664, MIL-STD-1553 or CAN.
• Cryptographic protocols and secure communication on constrained hardware.
• Qualified compilers and toolchains for Rust or Ada.

Eligibility

• Right to work in the European Union.
• Military obligations completed, or a lawful exemption, where they apply to you.