Alcides Fonseca

Jailbreaking for kids

Alcides Fonseca — Tue, 10 Nov 2026 09:38:23 +0000

Pamela Fox published her slide deck on what we need to change in the way we teach CS all across the different age ranges, starting from primary school and going up to the university degree.

Some of my colleagues were in disbelief that she included "Understanding how AI works" as a primary school objective.

Just like you can't prevent teenagers from lying about their birthdate and getting access to porn, you will not be able to prevent kids from using AI models, especially if Big Tech has their way with it and every product in your household is infused with a chatbot/agent.

The best way to make AI safe for kids is through education. You need to teach kids how AI works, and what its limits are and what you can do safely or not.

Dale Lane has this awesome project called Machine Learning for Kids where kids can write ML and AI applications using a scratch-like programming environment.

In today's video, Dale goes through jailbreaking, where the agent is supposed to keep a password protected, and the user tries different things to extract that password from a weak-willed agent.

So yes, you can teach primary school kids how AI works. And we should be doing this right now, not in a couple of years.

Can you leave a 5 star review?

Alcides Fonseca — Sat, 07 Nov 2026 12:49:50 +0000

Wizard of Id pulls a Black Mirror.

Full-stack verification is the new trend

Alcides Fonseca — Wed, 04 Nov 2026 23:59:50 +0000

There have been several recent announcements about formal verification of software and hardware, both using AI and for AI systems:

Harmonic announced last week that they are using their agent Aristotle for scalable verification of both software and hardware. For example, in a C library for big-number arithmetic, it was able to fix bugs and prove that a faster version was equivalent to the original. The person whose work I particularly follow in this area is Satnam Singh, who has worked on hardware verification for several years.
SF-Tensor announced that they were formalizing NVIDIA’s PTX language in Lean to prove the correctness of GPU kernels. SF-Tensor was founded by three brothers at the age of 19, after they had completed their BSc degrees at 16 while attending high school.
&Truth came out of stealth, announcing plans to use Lean to prove the correctness of AI-generated software. Key people involved include Clark Barrett, known for his work on cvc5 and CSLib; Ilya Sergey, known for Veil and his work on verification using separation logic; and Sebastian Ullrich, Lean’s second-in-command.
Theorem. and Anthropic worked together on verifying open-source software running on a RISC-V processor. Their work covered encode–decode round-tripping, idempotence, algebraic laws, differential testing, self-consistency, and equivalence to reference implementations. They also proved isolation properties of a sandbox built on the xv6 academic kernel.
AutoResearch.inc has also announced they have verified 7 web assembly tools down to ELF and sys calls (on x86-64 and RISC-V).

The common factor in these announcements is the goal of achieving full-stack formalization, either across the software stack or across a combination of software and hardware. In the past, verification was performed only on a small core of the software or on a simplified model of the actual software.

For reference, AWS’s access-control language, Cedar, had a Rust implementation running in production and a reference implementation—first in Dafny and later in Lean—that was verified for correctness.

One approach would be to develop Cedar entirely in Lean, compile to C, and deploy the generated C code in production. In addition to the formal model, we would write an optimized and full-featured implementation (which handles errors and messages more carefully, provides parsers for various formats, etc.) in Lean, and then prove the two equivalent. A key benefit of this approach is that we would formally verify—rather than just test—the equivalence of the deployed code and model. But there are significant downsides to writing production applications in Lean and deploying its generated C code. Lean is a new programming language, so it has a limited developer pool and lacks useful libraries available in mainstream languages. Debugging a failure might necessitate stepping through the generated C code and mapping it back to the Lean source, requiring expertise in C and Lean. Doing so could be particularly difficult if the failure is due to an interaction between handwritten code and Lean-generated C code. In addition, C is a memory-unsafe language, so a bug in the Lean compiler could lead to security issues.

— How We Built Cedar: A Verification-Guided Approach (April 2024)

Over the past year, I have been talking about liquid types as my personal preference for program verification. Liquid types are a restricted form of value-dependent types whose constraints can be checked automatically using SMT solvers. This is my sweet spot: you get much of the benefit of an expressive type system in which you can express properties such as typestate, preventing methods from being called when an object is in the wrong state—for example, calling read() after close(). And it comes at a much lower cost, especially because you do not have to write the proofs: the SMT solver takes care of that.¹

Until a few months ago, this trade-off was very important: very few people in the world had the expertise and time to undertake the full verification of a large open-source project (props to the seL4 folks!). Frontier models’ superhuman ability to generate proofs has since eroded this moat, and subsidized token prices make this the perfect time to conduct these experiments. I have to admit that the image above, which I used in my recent slides, might no longer make sense. It might become relevant again when token prices rise—probably to reflect their actual costs—and we need to save time and tokens while still verifying properties we care about, without going all the way down to the machine-code level.²

Right now, if we pursue full-stack verification, we might need to write code in a verification-first language like Lean. Dafny and my own aeon could be candidates, but Lean’s functional programming model and the substantial funding the project receives make it the ideal candidate. Rocq enthusiasts might not like it, but extracting executable code to OCaml is not such a significant advantage in the real world.

But we need Lean to improve. Above all, we need faster type checking and a much better optimizer. That’s the part that Bend2 got right from the start—the next mainstream language will require both verification and speed.

Using proof combinators, you can use LiquidHaskell to achieve the same expressive power as Lean. Conversely, you can use Lean with only the grind tactic to achieve the same lower cost as liquid types. Here, I am considering each as it is typically used. ↩
I am convinced that people will not read the source code and will instead rely on new techniques to establish confidence in the generated code. ↩

How to express intent in aeon

Alcides Fonseca — Tue, 03 Nov 2026 13:35:15 +0000

I started developing Aeon back in 2018 as a playground for program synthesis. Holes (?x) are valid expression in aeon (def f (i:Int) : Int := i * 2 + ?x compiles successfully and, when ?x is evaluated at runtime, it opens a repl asking the user for the right expression). However, the main advantage of holes is when you run the aeon compiler with "--synthesizer", it tries to find a suitable expression for the holes in your program. This blog post covers the different methods you have to describe what you want a function to do. We've decided on the function-level for the specification as it is the most normal public (and private) API of your code.

Basic Types

Aeon is a (very strongly) typed language, so you always need to write the types of top-level functions.¹ As such, all proposed candidate expressions to replace ?hole need to type-check. So writing Int as the return type already specifies something about the missing code.

def double (x:Int) : Int := ?hole

Liquid Types

Aeon supports liquid types by refining a basic type with a predicate. In the case below we refine the returning type of the function Int with the predicate that it needs to be equal to twice the value of x. Because Liquid Types can refer to other values in the program (such as function arguments), they are (value-)dependent types, but following a different discipline than the (full) dependent types you find in Lean, Rocq or Idris.

def double (x:Int) : {r:Int | r == x + x} := ?hole

So far, this definition covers both Refinement Types and Liquid Types. The main distinction of the two is that the refinements in Liquid Types need to be drawn from a decidable logic, so an SMT solver can give you a definitive answer of whether it type checks or not.

Liquid types guide synthesis directly in approaches such as Synquid and Liquid Tree Automata. In Aeon, their logical predicates can also be translated into constraints for SMT solving with Z3, syntax-guided synthesis (SyGuS), polynomial synthesis, and OR-Tools’ CP-SAT solver. Liquid Types are also used in our own custom synthesis algorithms that combine evolutionary search and liquid types.

Natural language documentation

Aeon also supports AeonDoc, using the @doc decorator to annotate a natural-language description of the function. We can take this documentation as input to a synthesis method (currently, only LLM-based synthesizers support @doc). This documentation complements any type that constrains the hole already.

@doc("Doubles the input.")
def double (x:Int) : Int := ?hole

Examples or test cases.

Aeon supports the decorator @example that takes a boolean predicate about the execution of the final synthesized function.

@example(double 3 = 6)
@example(double 5 = 10)
def double (x:Int) : Int := ?hole

Input–output examples guide many synthesis approaches: automata-based methods such as AFTA use them to prune spaces of candidate programs; top-down methods such as Myth or Decision Trees propagate examples into smaller synthesis subproblems; and bottom-up methods such as BUSTLE compose programs from smaller expressions evaluated on those examples. Examples also define fitness functions for genetic programming and provide training data for decision-tree learning, which learns conditional rules mapping inputs to outputs.

Decision Trees and Genetic Programming, coming from the Machine Learning backgrounds, assume that some examples might be wrong so they are more permissive. Other methods typically search for a solution that covers all examples. In this case, only noise-supporting methods can handle contradictory examples.

Because writing examples can be tedious, you can use CSV data directly or through an auxiliary file (@csv_data("1.0,2.0\n3.0,6.0\n4.0,8.0") or @csv_file("double.csv").

Optimization goals

@minimize_int(abs $ (double 4) - (4 * 2))
@minimize_int(abs $ (double 5) - (5 * 2))
def double (x:Int) : {r:Int | r = x + x} := ?hole

Aeon supports multiple maximize and minimize decorators to express optimization goals. We might know a given ideal target for the minimization criteria or not (for open problems). This example is the former, where you cannot have a value lower than 0. However, if you were to maximize the return value of a function that returns prime numbers, you would have no target value.

When multiple objectives are set, we consider this a multi-objective optimization problem and each algorithm typically returns the Pareto set, containing solutions that no other candidate is better in all axis. Genetic Programming and OR-Tools solvers have these features built-in. Recent Genetic Programming approaches have recommended Lexicase-selection instead of a Pareto tournament, but my own experience does not confirm this recommendation. If you are going to evaluate all objectives, then lexicase selection might make sense, but because tournaments only evaluate one objective for few good candidates, it ends up being more computational cheaper, and more time is left for exploration.

A big advantage of examples and optimization constraints over liquid types is that you can write any aeon expression that you want (such as multiplication of variables i*j). Because Liquid Types are limited to decidable theories, you cannot write² this multiplication and other types of expressions and you are limited to linear integer arithmetic, arrays, uninterpreted functions and other SMT theories.

Property-based Tests

Property-based testing is the idea that instead of writing concrete input and output examples, you write properties that relate them, and have random inputs generated to validate those properties. For me, it is very similar, if not the same, as Metamorphic testing.

def double (x:Int) : Int := ?hole

@property(100)
def prop_double_is_bigger (x:Int | x > 0) : Bool := double x > x

In this example, the body of the double function will have to work with 100 randomly-generated inputs and return a value that complies with the state property every single time.

Results

You can either run aeon on the command line, selecting the synthesizer method with -s (python -m aeon multi_objective.ae -s gp --budget 10), or use an LSP editor to ask the compiler to synthesize using a particular method. If you are using VSCode, you have an extra interface to explore program synthesis.

The first specification yielded def double (x:Int) : Int := 1, which matches exactly what we asked it to return: an Integer. When using the other specifications we got a variety of solutions: x+x, 2*x and x+x+0. But this is with a very simple specification that I would assume any synthesizer should be able to generate. Larger examples are left to the reader (or to the next blog post).

Non-functional requirements

All of the intent that we have expressed for far was related to functional correctness. But software developers know that non-functional properties can be equally important in some projects. As such, we are adding support for different forms of expressing quality properties. In particular, we already support @minimize_cputime(expression) and @minimize_energy(expression) for minimizing execution time and energy consumption respectively. Despite this support, the example above is too simple and trivial that the measurement overhead is many times that of the execution. I would only recommend using these advanced decorators for larger programs.

And aeon also supports other properties, you just need to write the code that translates the candidate function into a measure of that quality, using the example or optimization decorators.

Happy synthesizing!

This restriction comes from Liquid Types. ↩
Actually you can, but you will get a warning. This is an UX improvement we are making based on our paper on challenges of Liquid Types adoption. ↩

Habitação Insustentável em Portugal

Alcides Fonseca — Tue, 27 Oct 2026 14:26:59 +0000

A realidade da habitação em Portugal é completamente fora deste mundo. A minha geração e a mais nova não consegue pagar o custo que a habitação tem sido nas grandes cidades, nem no Algarve.

O Ivo Bernardo fez uma análise da situação da habitação em Portugal, baseado em números públicos de uma variedade de fontes.

Public housing: this is where the data sides most with the protesters. Social rental housing is 1.1% of dwellings in Portugal, against an EU average of 8%. At €150,000 per home, 3% financing and public land, a cost-rent home in Lisbon breaks even at about €10.9/m² a month, 35% below the city’s median new rent. It can almost pay for itself exactly where it’s needed most. Remember the €1.74 billion NHR cost in 2024? That’s roughly 11,600 of those homes. In one year.

Vacant homes: worth chasing, in the right places. The 100,000-plus recoverable homes in pressure municipalities are real.

Limiting investment funds: I can’t back it or reject it, because the data doesn’t exist. Before we legislate, we need to measure.

— The housing crisis in Europe pt1 by Ivo Bernardo

Por sua vez, o João Tomé usa também dados reais para analisar a questão das casas vazias.

Em 2021, quase 249 mil casas estavam vagas por outros motivos, fora do mercado, em edifícios sem necessidade de reparação ou apenas com reparações ligeiras. Os dados ajudam a localizar uma possibilidade de resposta à falta de habitação. Ainda não dizem quantas dessas portas se podem abrir. As experiências de outros países ajudam a escolher o que tentar: apoiar obras, gerir o arrendamento e reforçar a oferta nas zonas com procura.

— Quantas casas vazias podem voltar a ter gente? por João Tomé

O artigo inclui ainda uma tabela com referências para medidas que foram implementadas noutros países e os resultados.

De ambos os estudos, a minha conclusão é que precisamos de mais construção e reabilitação, precisamos de melhores números e acompanhamento da situação e, sobretudo, precisamos de descentralizar a população nas grandes áreas metropolitanas.

Infelizmente, manifestações de tendas dão-me pouca confiança que algo vá mudar. Mas termos novas iniciativas políticas que trabalhem estes desafios parece-me algo com maior probabilidade de funcionar. O resultado na Sérvia de um movimento estudantil ganhar as eleições inspira-me confiança, mas não podemos ter a taxa de abstenção que tem sido habitual no nosso país.

Training people in AI Safety

Alcides Fonseca — Tue, 27 Oct 2026 12:36:05 +0000

As AI technology gets adopted at a never-seen pace, we also need more people to work on AI Safety to make sure that AI applications are actually safe and aligned.

Because AI generates content and decisions faster than humans, this is a very interesting research problem: humans cannot verify AI alone, so we need smarter technology to do it.

In the interview below Ryan Kidd, the CEO of MATS, talks about the efforts they (and others) are doing to train people in AI Safety. Throughout the conversation he also addresses how many of these AI Safety companies/non-profits have been founded, and even goes into neural networks vs evolutionary algorithms.

But AI Safety is a very large umbrella that encompasses soft skills like Policy Making and writing Model Cards to more technical challenges like interpreting neural networks or building guardrails.

Ankur Pandey argues that AI Safety training is not focusing on building tools and that's probably where the gains are for society. I actually believe existing researchers from technical domains (like formal verification) are equipped to build the tools, they just need funding and support. As an example, Harmonic has been doing interesting stuff recently and I know they recruited the right people.

Unfortunately for those of us who do not want to relocate, many of these AI Safety companies are in-person in Berkeley, DC, Cambridge, NYC and London (with India and Singapore also investing in these areas). If I was funding these efforts, I would hire remotely and I would try to get funding from NATO/EU/UNESCO and other multinational organizations.

As for training, I think we should make sure that all universities offer an AI Safety course at least at the Masters level, but here I am, daydreaming again.

What are the measurable outcomes of researchers in the AI world

Alcides Fonseca — Tue, 20 Oct 2026 13:21:55 +0000

Early this month, OpenAI has released several papers answering decades old problems to which mathematicians have dedicated their own careers. This NYT piece on Terrence Tao (who first supported AI when it was AI to help humans in the process of discovery, but shunned them when it became apparent that they were looking for the discovery for discovery sake, and not for the journey of learning.

Personally, I think it's a matter of changing the training dataset to learn in the process, and AI can do maths the human way very soon.

OpenAI has tried to ask for forgiveness by pledging 5 million to mathematics, maybe hoping that they come back in tokens. On the other side of the duopoly, Anthropic has donated shares to the public good, which seems to me impossible to manage.

AI is here to stay, and it's only a matter of us, humans, mathematicians or software developers finding our raison d'être and learning to communicate with AI in a way that it also advances our knowledge.

At the heart of the crisis in the profession is a menacing question. If solving hard problems is a mission of math, what happens when machines can do it faster? So much of higher math — hiring, promotions, graduate training and acclaim — is based on the difficulty, quality and the impact of papers (the written documents explaining proofs) that a mathematician produces.

The consensus is that A.I.-assisted problem solving is the inevitable future, but no one knows exactly what that new world will look like. “Deep uncertainty will persist in these next years,” a draft report by a group of mathematicians meeting at Harvard on Ph.D. education concluded last month.

— Elisabeth Bumiller on Terry Tao Is on the Front Lines of the Debate Over AI and the Future of Math

This is a completely different subject. Academics created a bean counting system to assess progress that is completely fake. Research is a high-risk activity, like Venture Capital. You invest in many different projects and teams, hoping that one out of 100/1000/1 million succeeds and has a huge impact on society. So you should be okay with the losses you take. It's part of the high-risk/high-reward system.

CoARA and Informatics-Europe provide recommendations to assess researchers: focus on the research and forget bean-counting. But even universities that are trying to adopt CoAra (like my employer, U. Lisbon) forget about the goal and come back to KPIs for fear that funding will be given based on KPIs.

Curiosity-driven research has been responsible for many important discoveries and inventions. So there should be a base funding for that. Then, there should be strategic funding for each country's long-term priorities (healthcare, transportation, defense). Meet with people and fund based on the team and the impact that the project might bring.

To assess researchers, let their peers assess them through conversations and presentations about their work. Do not rely on publication counts and other metrics that can be gamed. And if you are not qualified to evaluate a researcher, maybe you shouldn't had hired them in the first place.

Lisbon through the ages

Alcides Fonseca — Tue, 20 Oct 2026 13:10:31 +0000

Lessons learned building Fronteira

Alcides Fonseca — Fri, 16 Oct 2026 12:35:39 +0000

I designed a harness built on top of dependent types that uses information-flow policies to prevent attacks involving the lethal trifecta. However, expecting users to write liquid types was unrealistic, and creating a custom SDK for every external interface—filesystems, APIs, internet search and MCP tools—was not practical.

Following feedback from Lisbon.ai (thanks, Nuno, Fred, Sérgio and David), I started building Fronteira to make these technical ideas accessible to a wider audience.

What is Fronteira?

Fronteira is an MCP proxy that acts as a behavioral firewall. You log in through the browser and add integrations with GitHub, Gmail and other services through their MCP servers. You authenticate your harnesses with Fronteira and automatically get access to all your configured MCP servers. You also get portability across harnesses, but that is just a side effect.

The main advantage of Fronteira is that all MCP interactions go through it, allowing it to track behavior across multiple MCP servers. You get tool-call logging for your harness for free—or, in an enterprise setting, for all your users. I have to admit that this was extremely useful when debugging Fronteira itself, as well as some custom MCP servers.

Because all the data is centralized, we can track where information flows. In particular, this allows Fronteira to stop attacks involving the lethal trifecta. Such an attack can occur when a prompt injection causes an agent to read private data through one tool and expose it to an external endpoint through another. Requiring all interactions to pass through MCP servers is a clear limitation, which I will address later.

Because there are countless MCP providers and possible combinations, each with its own schema, it is impossible for me to write a set of rules that prevents harmful actions for everyone. Instead, Fronteira allows you to write your rules in English and translates them into Guard DSL, a language evaluated deterministically on every interaction.

Users are not expected to write Guard DSL themselves. Instead, they write rules in natural language and can check that the resulting code matches their expectations. The language's usability could be improved, but it is sufficient for the prototypes I have built.

While the rule language is evaluated deterministically, it can invoke nondeterministic components that use decision models—currently JEV—to determine whether content contains trade secrets or medical information. There is also session-level tracking, such as read_private in the example. So far, I have not found anything I could not express, but I am sure that will happen as soon as someone else starts using it.

Limitations and Technical Lessons Learned

The first limitation is clear: top-level harnesses access the filesystem directly, browse the internet directly, control desktop apps and access APIs directly, usually through skills or other instructions. All these interactions bypass Fronteira, making it useless for day-to-day security in your harness.

Second, harnesses come with skills that assume the user is using the harness's official Gmail integration—for example, Codex's integration. If Gmail is only available through Fronteira's MCP endpoint, Codex will sometimes fail to find it out of the box. Deploying Fronteira in the wild would therefore require us to write many skills to change this default behavior.

I also learned that no one respects the fact that MCP tool lists can be dynamic according to the specification. Requests for the tool list can return different results throughout a conversation, but harnesses do not implement support for this. They load the tool list at the beginning and do not reload it unless explicitly asked. I understand the challenge: reloading it before every response would increase the load on MCP servers and add latency. I would like a flag in the response that forces clients to refresh the list.

Furthermore, the MCP schema can change at any time. There is assumption that MCP schemas do not ever change, but I wonder how reliable the assumption is. MCP does not have explicit versioning, although some providers use REST-style versioned endpoints such as /api/v1.

On the other hand, I do not want Fronteira to expose a million tools at all times. I would like it to receive the prompt, or some related information, and dynamically select the relevant tools. Tools forbidden by the rules could then be excluded from the context, rather than occupying space when any attempt to call them would result in an error.

The final technical lesson I learned is that I was too optimistic about trusting Codex with DevOps. I asked it to mirror another app's Django configuration for Fronteira, but it changed the server root, exposing my Resend token and allowing spammers to send spam through my account. The issue was easy to identify and fix, but I expected more from Codex. I also realized that I still do not have a security tool I can point at a deployment, rather than its source code!

Alternatives to Fronteira

I did not look at competitors before implementing Fronteira. This was not because of laziness or incompetence. It was simply not a priority: I wanted to build it regardless, to understand the challenges firsthand.

Behavioral Rules

I was aware of Dogwood, Amazon's temporal specification extension to the Cedar specification (mainly used for AWS access permissions).

Dogwood can require previous explicit approval for some actions. Approval is something I wanted to add to Fronteira from the start through a mobile app. The following temporal rule in Cedar permits a share sale only if the same stock and number of shares were approved within the past hour.

permit (
    principal,
    action == AgentCore::Action::"SellShares",
    resource
)
when temporal {
    formerly within 1h AgentCore::Action::"ApproveSale"::response{
        input.stock: context.input.stock,
        input.shares: context.input.shares,
        output.approved: true
    }
};

To address some of the same limitations as Fronteira, Amazon uses the Dogwood engine in the Strands SDK. By combining the policy engine with a sandbox, they prevent agents from circumventing the "firewall." This is still not foolproof: agents can use a remote browser MCP server to call APIs, avoiding detection.

The Invariant SDK features dataflow guardrails. Both Invariant and Cordon offer MCP proxies like Fronteira. They share the same limitations, but I would like to highlight some interesting language features such as quantifiers and loop detection.

Executor.sh is another MCP proxy that adds some interesting configurations. For instance, it allows you to create policies in typescript, requiring approval of actions, but also more interesting behaviors such as allowing you to undo sending an email in the next 5 minutes.

MCP Proxies with Static Rules

Mintive, previously MintMCP, is very similar to Fronteira, except that it does not support behavioral rules. You can still detect private information leaking through static rules, but you cannot prevent malicious sequences of individually harmless calls.

Both the Lasso Security MCP Gateway and WitnessAI are very similar to Mintive: they automatically manage MCP servers and can detect leaks of information identified as private.

MCP Firewall performs a similar role but also focuses on filtering MCP responses, treating their contents as untrusted because they may contaminate subsequent reasoning.

NVIDIA NeMo is another proxy that validates tool parameters and responses against a range of requirements. However, it does not relate different tool calls to one another except through custom code.

Endram is a proxy that decides whether each call requires manual approval, something Dogwood also supports alongside more complex features.

Both WSO2 and Microsoft Global Secure Access support Cedar-like access control lists for MCP servers, with tool- and prompt-level controls.

Agent Control allows you to create guardrails in Python. These operate at the level of individual tool calls, but Agent Control also integrates with external guardrail infrastructure, such as Dogwood, whose language is more expressive.

Language Specification

AgentSpec is a specification language like Fronteira's, with a more principled design but similar features. I would like to study properties of the language, particularly ways to provide feedback when users write inconsistent rules.

Others

IBM offers MCP ContextForge, a central gateway focused more on discoverability and observability. agentgateway is also mostly focused on observability. TrueFoundry focuses on the M×N problem—M harnesses connecting to N MCP servers—and observability.

LlamaFirewall is similar in that it can inspect traces of calls and detect malicious patterns. However, it does so using a BERT-style LLM, whereas Fronteira primarily supports deterministic analysis.

Comparison Summary

Approach	MCP proxying	Content guards	Behavioral / temporal guards
Fronteira	✅	✅	✅
Dogwood + Strands Box	🚫	✅	✅
Invariant + MCP Scan	✅	✅	✅
Executor.sh	✅	✅	✅
Cordon	✅	🚫	🟡
Mintive / MintMCP	✅	✅	🟡
Lasso MCP Gateway	✅	✅	🚫
WitnessAI	✅	✅	🚫
MCP Firewall	✅	✅	🟡
NVIDIA NeMo Guardrails	🚫	✅	🟡
Endram	✅	🟡	🚫
WSO2 MCP ACL policy	✅	🚫	🚫
Microsoft GSA MCP firewall	✅	🚫	🚫
Agent Control	🚫	✅	🟡
AgentSpec	🚫	🟡	🟡
IBM ContextForge	✅	🟡	🚫
agentgateway	✅	✅	🟡
TrueFoundry	✅	✅	🚫
LlamaFirewall	🚫	✅	✅ (probabilistically)

Conclusion

After this exercise, I no longer believe in MCP proxies as security boundaries for agents. MCP covers only part of an agent's interaction with the world. Another reason is that MCP is a leaky abstraction. Models are post-trained in specific MCP and skill contexts, so they will always prefer direct alternatives, creating friction for the user.

However, I strongly believe in the need for logic-based policies to control agents. Those policies should be enforced at the agent boundary and should probably be developed alongside the harnesses and models. I would love this enforcement to be harness-independent and provided by a third party. However, given how models are becoming increasingly harness-specific, I do not see that working in the long term.

If you have read this far, I am looking for a new opportunity where I can apply my research experience in programming languages, systems and different areas of artificial intelligence to improve the safety of agentic systems. If you are looking for someone with that background, along with the agency and pace of someone who has worked at several startups, you can find my contact details on this website.

If I were a Bank CTO (part 2)

Alcides Fonseca — Thu, 15 Oct 2026 08:03:32 +0000

I certainly would not hire 1,000 third-party consultants to help fix patches. I would probably rethink the architecture of the whole system and company, so that the exposed footprint is minimized. I would give proper training to the internal 3.000 people and power them with AI tooling (even if for monitoring and preventing attacks). And I would even consider open-sourcing the code.

But hiring a lot of (most likely under qualified) people to patch vulnerabilities is a losing game.