- Architect and principal author of aion (~6,200 of 6,450 commits), a declarative, multi-tenant application platform where AI agents are first-class participants under machine-checked contracts, together with the build and deploy substrate it runs on.6,200 commits
- Mechanized the normative specification in Lean 4: a 57-RFC suite reduced to a seven-proposition kernel, with 1,400+ machine-checked theorems across 570 modules covering permission algebra, bitemporal CRDT convergence, safe schema migration, and typed-expression soundness. Proofs run as Bazel test targets, so a spec regression fails CI like any other test.1,400+ proofs
- Stood up a self-hosted Buildbarn remote-execution and cache plane: cold clone to built in 175 s (vs. ~48-min GitHub Actions baseline), two bzlmod registries serving 100+ rules_* modules behind machine-checked conformance gates, blast-radius-scoped test selection as the merge gate, and SOC 2 evidence emitted as a control-plane byproduct.175 s
Software Engineering Leader
Matthew Marshall
Open to Ask
Answers only from published material. You see every question.
Featured
About
Passionate and detail-oriented software engineering leader with extensive experience in distributed systems, cloud-native architectures, and finance. Skilled in designing and optimizing high-performance systems, leading engineering teams, and delivering critical enterprise solutions. Proven track record in leading complex technical initiatives, implementing scalable architectures, and driving operational efficiency in fast-paced environments. References available upon request.
Experience
- Led the development of a microservices-based portfolio benchmarking engine using gRPC and Protobuf, supporting arbitrarily complex composite index calculations, real-time FX conversion, and flexible fund performance comparisons.
- Directed NSF-funded R&D as PI for two grants (1722276 and 1927042) focused on using symbolic AI and optimization to address climate-based financial risk management. Managed personnel, budgets, timelines, and reporting requirements.2 grants
- Optimized geospatial clustering algorithm for reinsurance customer, significantly reducing O(n2) runtime complexity for distance matrix calculations by using H3 as a discrete global grid system and parallelizing with TensorFlow.O(n²)
Freelance Full-Stack Software Developer · M Software Solutions LLC
- Advised data engineering team for 2 years at unicorn alternative protein company on data pipeline design in GCP.
- Developed serverless ETL in AWS Lambda for forensic accounting system, analyzing 30M transactions in PostgreSQL.
- Engineered performance and query enhancements for portfolio compliance alerts with 3x speed improvement.
- Fixed numerous bugs and stability/performance issues in the IMS C# and Java codebases.
- Designed integration testing and quality metrics for critical parts of the fund subscription and redemption processes.
- Deployed automated remote code coverage and instrumentation using WMI on Windows Server.
Skills
PythonJavaC#JavaScript/TypeScriptRustGoLean 4KafkaNATSSparkBeamDaskBigQueryPandasTensorFlowPyTorch