Research
The work itself.
We are not going to show you client logos. Our engagements are confidential and we are not going to invent references. What we can show you is the work: our papers, our articles, and every tool we have built, in the open, with its history.
Research papers
- Specifying Algorithms Using Non-Deterministic ComputationsProgram VerificationInference
- Deductive Verification as an Alternative to Push-Button TechnologiesProgram VerificationSMTModel checking
- Verification-driven developmentProgram VerificationVerification Driven Development
- Program Verification: background and notationMathematicsProgram VerificationFoundations
Technical articles
- New Approach to Formal Verification Methods for Combating Vulnerabilities in Smart ContractsProgram VerificationFormal VerificationFormal Specification
- The Fundamental Architecture of LLMs: A Perspective Through Information Theory and Lossy CompressionInformation TheoryAlgorithmsLLM
- Monolithic Architecture vs. Formal Verification: The Combinatorial Explosion ProblemArchitectureFormal VerificationStellar
- Pocket exchange with UniswapX and 1inch FusionDeFiUniswap1inch
- Preparing Polkadot pallet Balances for Formal VerificationPolkadotFormal VerificationFormal Specification
- Introduction to Fully Homomorphic EncryptionMathematicsCryptographyFully Homomorphic Encryption
Code we maintain in the open
Everything below is public. The star counts are rounded down.
| Repository | What it is | Language | Stars |
|---|---|---|---|
| inference | The Inference programming language and compiler | Rust | 100+ |
| soroban-security-portal | The Stellar Security Portal: Soroban audit history, tooling and reviewers | TypeScript | 50+ |
| inference-language-spec | The Inference language specification | Spec | — |
| book | The Inference book | JavaScript | — |
| tree-sitter-inference | Inference grammar for tree-sitter | JavaScript | — |
| inf-wasm-tools | WebAssembly tooling with non-deterministic operation support | Rust | — |
| soroban-ret | Soroban smart contract reverse-engineering tool | Rust | — |
| pallet-balances-formal-verification | Formal specification and verification of Polkadot's pallet_balances | WebAssembly | — |
Grants and ecosystem work
Our open-source work has been funded through competitive project grants, including work in the Stellar ecosystem and verification work on Polkadot's pallet_balances. These are project grants, not partnerships and not endorsements, and we describe them that way everywhere. What they do show is that independent technical reviewers read our proposals and funded them.
Start a conversation
We are not going to show you client logos. Our engagements are confidential and we are not going to invent references. What we can show you is the work: our papers, our articles, and every tool we have built, in the open, with its history.